1 /-
2 Copyright (c) 2018 Kenny Lau. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Kenny Lau
5
6 Free groups as a quotient over the reduction relation `a * x * x⁻¹ * b = a * b`.
7
8 First we introduce the one step reduction relation
9 `free_group.red.step`: w * x * x⁻¹ * v ~> w * v
10 its reflexive transitive closure:
11 `free_group.red.trans`
12 and proof that its join is an equivalence relation.
13
14 Then we introduce `free_group α` as a quotient over `free_group.red.step`.
15 -/
16 import logic.relation
src └────────────┘
17 import algebra.group algebra.group_power
src └───────────┘ └─────────────────┘
18 import data.fintype data.list.basic
src └──────────┘ └─────────────┘
19 import group_theory.subgroup
src └───────────────────┘
20 open relation
21
22 universes u v w
23
24 variables {α : Type u}
id ┴
typ ┴
25
26 local attribute [simp] list.append_eq_has_append
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
doc └──┘
27
28 namespace free_group
29 variables {L L₁ L₂ L₃ L₄ : list (α × bool)}
id └──┘ ┴ └──┘
src └──┘ ┴ └──┘
typ └──┘ ┴ └──┘
30
31 /-- Reduction step: `w * x * x⁻¹ * v ~> w * v` -/
32 inductive red.step : list (α × bool) → list (α × bool) → Prop
id └──┘ ┴ └──┘ └──┘ ┴ └──┘
src └──┘ ┴ └──┘ └──┘ ┴ └──┘
typ └──┘ ┴ └──┘ └──┘ ┴ └──┘
33 | bnot {L₁ L₂ x b} : red.step (L₁ ++ (x, b) :: (x, bnot b) :: L₂) (L₁ ++ L₂)
id └┘ └┘ ┴ ┴ └┘ └┘ ┴┴ ┴ └┘ ┴┴ └──┘ ┴ └┘ └┘ └┘ └┘ └┘
src └┘ ┴ └┘ ┴ └──┘ └┘ └┘
typ └┘ └┘ ┴ ┴ └┘ └┘ ┴┴ ┴ └┘ ┴┴ └──┘ ┴ └┘ └┘ └┘ └┘ └┘
34 attribute [simp] red.step.bnot
id └───────────┘
src └───────────┘
typ └───────────┘
doc └──┘
35
36 /-- Reflexive-transitive closure of red.step -/
37 def red : list (α × bool) → list (α × bool) → Prop := refl_trans_gen red.step
id └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └────────────┘ └──────┘
src └──┘ ┴ └──┘ └──┘ ┴ └──┘ └────────────┘ └──────┘
typ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘ └────────────┘ └──────┘
doc └────────────┘ └──────┘
38
39 @[refl] lemma red.refl : red L L := refl_trans_gen.refl
id └─┘ ┴ ┴ └─────────────────┘
src └──┘ └─┘ └─────────────────┘
typ └─┘ ┴ ┴ └─────────────────┘
doc └──┘ └─┘
40 @[trans] lemma red.trans : red L₁ L₂ → red L₂ L₃ → red L₁ L₃ := refl_trans_gen.trans
id └─┘ └┘ └┘ └─┘ └┘ └┘ └─┘ └┘ └┘ └──────────────────┘
src └───┘ └─┘ └─┘ └─┘ └──────────────────┘
typ └─┘ └┘ └┘ └─┘ └┘ └┘ └─┘ └┘ └┘ └──────────────────┘
doc └───┘ └─┘ └─┘ └─┘
41
42 namespace red
43
44 /-- Predicate asserting that word `w₁` can be reduced to `w₂` in one step, i.e. there are words
45 `w₃ w₄` and letter `x` such that `w₁ = w₃xx⁻¹w₄` and `w₂ = w₃w₄` -/
46 theorem step.length : ∀ {L₁ L₂ : list (α × bool)}, step L₁ L₂ → L₂.length + 2 = L₁.length
id ┴ └──┘ ┴ ┴ └──┘ └──┘ └┘ └┘ └┘└─────┘ ┴ ┴ └┘└─────┘
src └──┘ ┴ └──┘ └──┘ └─────┘ ┴ ┴ └─────┘
typ ┴ └──┘ ┴ ┴ └──┘ └──┘ └┘ └┘ └┘└─────┘ ┴ ┴ └┘└─────┘
doc └──┘
47 | _ _ (@red.step.bnot _ L1 L2 x b) := by rw [list.length_append, list.length_append]; refl
id └───────────┘ └────────────────┘ └────────────────┘
src └───────────┘ └──┘└────────────────┘└┘└────────────────┘┴ └────
typ └───────────┘ └──┘└────────────────┘└┘└────────────────┘┴ └────
doc └──┘ └┘ ┴ └────
txt └──┘ └┘ ┴ └────
par └──┘ └┘ ┴ └────
pid └┘ └┘ ┴ └
st └─────────────────────┘└──────────────────┘┴└──────
48
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
49 @[simp] lemma step.bnot_rev {x b} : step (L₁ ++ (x, bnot b) :: (x, b) :: L₂) (L₁ ++ L₂) :=
id └──┘ └┘ └┘ ┴┴ └──┘ ┴ └┘ ┴┴ ┴ └┘ └┘ └┘ └┘ └┘
src └──┘ └┘ ┴ └──┘ └┘ ┴ └┘ └┘
typ └──┘ └┘ └┘ ┴┴ └──┘ ┴ └┘ ┴┴ ┴ └┘ └┘ └┘ └┘ └┘
doc └──┘ └──┘
50 by cases b; from step.bnot
id ┴ └───────┘
src └────┘ └───┘└───────┘└
typ └────┘┴ └───┘└───────┘└
doc └────┘ └───┘ └
txt └────┘ └───┘ └
par └────┘ └───┘ └
pid ┴ └───┘ └
st └────────────────────────
51
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
52 @[simp] lemma step.cons_bnot {x b} : red.step ((x, b) :: (x, bnot b) :: L) L :=
id └──────┘ ┴┴ ┴ └┘ ┴┴ └──┘ ┴ └┘ ┴ ┴
src └──────┘ ┴ └┘ ┴ └──┘ └┘
typ └──────┘ ┴┴ ┴ └┘ ┴┴ └──┘ ┴ └┘ ┴ ┴
doc └──┘ └──────┘
53 @step.bnot _ [] _ _ _
id └───────┘ └┘
src └───────┘ └┘
typ └───────┘ └┘
54
55 @[simp] lemma step.cons_bnot_rev {x b} : red.step ((x, bnot b) :: (x, b) :: L) L :=
id └──────┘ ┴┴ └──┘ ┴ └┘ ┴┴ ┴ └┘ ┴ ┴
src └──────┘ ┴ └──┘ └┘ ┴ └┘
typ └──────┘ ┴┴ └──┘ ┴ └┘ ┴┴ ┴ └┘ ┴ ┴
doc └──┘ └──────┘
56 @red.step.bnot_rev _ [] _ _ _
id └───────────────┘ └┘
src └───────────────┘ └┘
typ └───────────────┘ └┘
57
58 theorem step.append_left : ∀ {L₁ L₂ L₃ : list (α × bool)}, step L₂ L₃ → step (L₁ ++ L₂) (L₁ ++ L₃)
id ┴ └──┘ ┴ ┴ └──┘ └──┘ └┘ └┘ └──┘ └┘ └┘ └┘ └┘ └┘ └┘
src └──┘ ┴ └──┘ └──┘ └──┘ └┘ └┘
typ ┴ └──┘ ┴ ┴ └──┘ └──┘ └┘ └┘ └──┘ └┘ └┘ └┘ └┘ └┘ └┘
doc └──┘ └──┘
59 | _ _ _ red.step.bnot := by rw [← list.append_assoc, ← list.append_assoc]; constructor
id └───────────┘ └───────────────┘ └───────────────┘
src └───────────┘ └────┘└───────────────┘└──┘└───────────────┘┴ └───────────
typ └───────────┘ └────┘└───────────────┘└──┘└───────────────┘┴ └───────────
doc └────┘ └──┘ ┴ └───────────
txt └────┘ └──┘ ┴ └───────────
par └────┘ └──┘ ┴ └───────────
pid └──┘ └──┘ ┴ └
st └──────────────────────┘└───────────────────┘┴└─────────────
60
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
61 theorem step.cons {x} (H : red.step L₁ L₂) : red.step (x :: L₁) (x :: L₂) :=
id └──────┘ └┘ └┘ └──────┘ ┴ └┘ └┘ ┴ └┘ └┘
src └──────┘ └──────┘ └┘ └┘
typ └──────┘ └┘ └┘ └──────┘ ┴ └┘ └┘ ┴ └┘ └┘
doc └──────┘ └──────┘
62 @step.append_left _ [x] _ _ H
id └──────────────┘ ┴┴┴ ┴
src └──────────────┘ ┴ ┴
typ └──────────────┘ ┴┴┴ ┴
63
64 theorem step.append_right : ∀ {L₁ L₂ L₃ : list (α × bool)}, step L₁ L₂ → step (L₁ ++ L₃) (L₂ ++ L₃)
id ┴ └──┘ ┴ ┴ └──┘ └──┘ └┘ └┘ └──┘ └┘ └┘ └┘ └┘ └┘ └┘
src └──┘ ┴ └──┘ └──┘ └──┘ └┘ └┘
typ ┴ └──┘ ┴ ┴ └──┘ └──┘ └┘ └┘ └──┘ └┘ └┘ └┘ └┘ └┘ └┘
doc └──┘ └──┘
65 | _ _ _ red.step.bnot := by simp
id └───────────┘
src └───────────┘ └────
typ └───────────┘ └────
doc └────
txt └────
par └────
pid └
st └─────
66
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
67 lemma not_step_nil : ¬ step [] L :=
id ┴ └──┘ └┘ ┴
src ┴ └──┘ └┘
typ ┴ └──┘ └┘ ┴
doc └──┘
68 begin
st └─────
69 generalize h' : [] = L',
id └┘
src └──────────────┘└┘┴ ┴
typ └──────────────┘└┘┴ ┴
doc └──────────────┘ ┴ ┴
txt └──────────────┘ ┴ ┴
par └──────────────┘ ┴ ┴
pid └─┘└┘┴ ┴ ┴
st ────────────────────────┘└─
70 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
71 cases h with L₁ L₂,
id ┴
src └────┘ └─────────┘
typ └────┘┴└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ───────────────────┘└─
72 simp [list.nil_eq_append_iff] at h',
id └────────────────────┘
src └────┘└────────────────────┘└─────┘
typ └────┘└────────────────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴┴ ┴┴└───┘
st ────────────────────────────────────┘└─
73 contradiction
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───────────────┘
74 end
st └─┘
75
76 lemma step.cons_left_iff {a : α} {b : bool} :
id ┴ └──┘
src └──┘
typ ┴ └──┘
77 step ((a, b) :: L₁) L₂ ↔ (∃L, step L₁ L ∧ L₂ = (a, b) :: L) ∨ (L₁ = (a, bnot b)::L₂) :=
id └──┘ ┴┴ ┴ └┘ └┘ └┘ ┴ ┴┴┴ └──┘ └┘ ┴ ┴ └┘ ┴ ┴┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴┴ └──┘ ┴ └┘└┘
src └──┘ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └┘
typ └──┘ ┴┴ ┴ └┘ └┘ └┘ ┴ ┴┴┴ └──┘ └┘ ┴ ┴ └┘ ┴ ┴┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴┴ └──┘ ┴ └┘└┘
doc └──┘ └──┘
78 begin
st └─────
79 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
80 { generalize hL : ((a, b) :: L₁ : list _) = L,
id ┴┴ ┴ └┘ └──┘
src └──────────────┘ ┴ └┘ └┘ ┴ └─┘└──┘└──┘ ┴
typ └──────────────┘ ┴┴└┘┴└┘ ┴└┘└─┘└──┘└──┘ ┴
doc └──────────────┘ └┘ └┘ ┴ └─┘ └──┘ ┴
txt └──────────────┘ └┘ └┘ ┴ └─┘ └──┘ ┴
par └──────────────┘ └┘ └┘ ┴ └─┘ └──┘ ┴
pid └─┘└┘┴ └┘ └┘ ┴ └─┘ └──┘ ┴
st ───┘└─────────────────────────────────────────┘└─
81 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
82 rcases h with ⟨_ | ⟨p, s'⟩, e, a', b'⟩,
id ┴
src └─────┘ └────────────────────────────┘
typ └─────┘┴└────────────────────────────┘
doc └─────┘ └────────────────────────────┘
txt └─────┘ └────────────────────────────┘
par └─────┘ └────────────────────────────┘
pid ┴ └────────────────────────────┘
st ─────────────────────────────────────────┘└─
83 { simp at hL, simp [*] },
src └────────┘ └───────┘
typ └────────┘ └───────┘
doc └────────┘ └───────┘
txt └────────┘ └───────┘
par └────────┘ └───────┘
pid ┴└───┘ ┴└─┘┴
st ─────┘└────────┘└─────────┘└┘└
84 { simp at hL,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└───┘
st ───────────────┘└─
85 rcases hL with ⟨rfl, rfl⟩,
id └┘
src └─────┘ └──────────────┘
typ └─────┘└┘└──────────────┘
doc └─────┘ └──────────────┘
txt └─────┘ └──────────────┘
par └─────┘ └──────────────┘
pid ┴ └──────────────┘
st ──────────────────────────────┘└─
86 refine or.inl ⟨s' ++ e, step.bnot, _⟩,
id └────┘ └┘ └┘ ┴ └───────┘
src └─────┘└────┘┴ ┴└┘┴ └┘└───────┘└──┘
typ └─────┘└────┘┴ └┘┴└┘┴┴└┘└───────┘└──┘
doc └─────┘ ┴ ┴ ┴ └┘ └──┘
txt └─────┘ ┴ ┴ ┴ └┘ └──┘
par └─────┘ ┴ ┴ ┴ └┘ └──┘
pid ┴ ┴ ┴ ┴ └┘ └──┘
st ──────────────────────────────────────────┘└─
87 simp } },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────┘└──┘└
88 { assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
89 rcases h with ⟨L, h, rfl⟩ | rfl,
id ┴
src └─────┘ └─────────────────────┘
typ └─────┘┴└─────────────────────┘
doc └─────┘ └─────────────────────┘
txt └─────┘ └─────────────────────┘
par └─────┘ └─────────────────────┘
pid ┴ └─────────────────────┘
st ──────────────────────────────────┘└─
90 { exact step.cons h },
id └───────┘ ┴
src └────┘└───────┘┴ ┴
typ └────┘└───────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────┘└────────────────┘└┘└
91 { exact step.cons_bnot } }
id └────────────┘
src └────┘└────────────┘┴
typ └────┘└────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────┘└───
92 end
st ──┘
93
94 lemma not_step_singleton : ∀ {p : α × bool}, ¬ step [p] L
id ┴ ┴ ┴ └──┘ ┴ └──┘ ┴┴┴ ┴
src ┴ └──┘ ┴ └──┘ ┴ ┴
typ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴┴┴ ┴
doc └──┘
95 | (a, b) := by simp [step.cons_left_iff, not_step_nil]
id ┴ └────────────────┘ └──────────┘
src ┴ └────┘└────────────────┘└┘└──────────┘└─
typ ┴ └────┘└────────────────┘└┘└──────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────────────────────────────
96
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
97 lemma step.cons_cons_iff : ∀{p : α × bool}, step (p :: L₁) (p :: L₂) ↔ step L₁ L₂ :=
id ┴ ┴ └──┘ └──┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └──┘ └┘ └┘
src ┴ └──┘ └──┘ └┘ └┘ ┴ └──┘
typ ┴ ┴ └──┘ └──┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └──┘ └┘ └┘
doc └──┘ └──┘
98 by simp [step.cons_left_iff, iff_def, or_imp_distrib] {contextual := tt}
id └────────────────┘ └─────┘ └────────────┘ └┘
src └────┘└────────────────┘└┘└─────┘└┘└────────────┘└┘ └────────────┘└┘└─
typ └────┘└────────────────┘└┘└─────┘└┘└────────────┘└┘ └────────────┘└┘└─
doc └────┘ └┘ └┘ └┘ └────────────┘ └─
txt └────┘ └┘ └┘ └┘ └────────────┘ └─
par └────┘ └┘ └┘ └┘ └────────────┘ └─
pid ┴┴ └┘ └┘ ┴┴ └────────────┘ ┴└
st └──────────────────────────────────────────────────────────────────────
99
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
100 lemma step.append_left_iff : ∀L, step (L ++ L₁) (L ++ L₂) ↔ step L₁ L₂
id ┴ └──┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └──┘ └┘ └┘
src └──┘ └┘ └┘ ┴ └──┘
typ ┴ └──┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └──┘ └┘ └┘
doc └──┘ └──┘
101 | [] := by simp
id └┘
src └┘ └───┘
typ └┘ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
102 | (p :: l) := by simp [step.append_left_iff l, step.cons_cons_iff]
id └┘ └──────────────────┘ ┴ └────────────────┘
src └┘ └────┘ ┴ └┘└────────────────┘└─
typ └┘ └────┘└──────────────────┘┴┴└┘└────────────────┘└─
doc └────┘ ┴ └┘ └─
txt └────┘ ┴ └┘ └─
par └────┘ ┴ └┘ └─
pid ┴┴ ┴ └┘ ┴└
st └──────────────────────────────────────────────────
103
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
104 private theorem step.diamond_aux : ∀ {L₁ L₂ L₃ L₄ : list (α × bool)} {x1 b1 x2 b2},
id ┴ └──┘ ┴ ┴ └──┘ └┘ └┘ └┘ └┘
src └──┘ ┴ └──┘
typ ┴ └──┘ ┴ ┴ └──┘ └┘ └┘ └┘ └┘
105 L₁ ++ (x1, b1) :: (x1, bnot b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, bnot b2) :: L₄ →
id └┘ └┘ ┴└┘ └┘ └┘ ┴└┘ └──┘ └┘ └┘ └┘ ┴ └┘ └┘ ┴└┘ └┘ └┘ ┴└┘ └──┘ └┘ └┘ └┘
src └┘ ┴ └┘ ┴ └──┘ └┘ ┴ └┘ ┴ └┘ ┴ └──┘ └┘
typ └┘ └┘ ┴└┘ └┘ └┘ ┴└┘ └──┘ └┘ └┘ └┘ ┴ └┘ └┘ ┴└┘ └┘ └┘ ┴└┘ └──┘ └┘ └┘ └┘
106 L₁ ++ L₂ = L₃ ++ L₄ ∨ ∃ L₅, red.step (L₁ ++ L₂) L₅ ∧ red.step (L₃ ++ L₄) L₅
id └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘┴ └──────┘ └┘ └┘ └┘ └┘ ┴ └──────┘ └┘ └┘ └┘ └┘
src └┘ ┴ └┘ ┴ ┴ ┴ └──────┘ └┘ ┴ └──────┘ └┘
typ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘┴ └──────┘ └┘ └┘ └┘ └┘ ┴ └──────┘ └┘ └┘ └┘ └┘
doc └──────┘ └──────┘
107 | [] _ [] _ _ _ _ _ H := by injections; subst_vars; simp
id └┘ └┘
src └┘ └┘ └────────┘ └────────┘ └───┘
typ └┘ └┘ └────────┘ └────────┘ └───┘
doc └────────┘ └────────┘ └───┘
txt └────────┘ └────────┘ └───┘
par └────────┘ └────────┘ └───┘
pid ┴
st └────────────────────────────┘
108 | [] _ [(x3,b3)] _ _ _ _ _ H := by injections; subst_vars; simp
id └┘ ┴┴ ┴
src └┘ ┴┴ ┴ └────────┘ └────────┘ └───┘
typ └┘ ┴┴ ┴ └────────┘ └────────┘ └───┘
doc └────────┘ └────────┘ └───┘
txt └────────┘ └────────┘ └───┘
par └────────┘ └────────┘ └───┘
pid ┴
st └────────────────────────────┘
109 | [(x3,b3)] _ [] _ _ _ _ _ H := by injections; subst_vars; simp
id ┴┴ ┴ └┘
src ┴┴ ┴ └┘ └────────┘ └────────┘ └───┘
typ ┴┴ ┴ └┘ └────────┘ └────────┘ └───┘
doc └────────┘ └────────┘ └───┘
txt └────────┘ └────────┘ └───┘
par └────────┘ └────────┘ └───┘
pid ┴
st └────────────────────────────┘
110 | [] _ ((x3,b3)::(x4,b4)::tl) _ _ _ _ _ H :=
id └┘ ┴ └┘┴ └┘
src └┘ ┴ └┘┴ └┘
typ └┘ ┴ └┘┴ └┘
111 by injections; subst_vars; simp; right; exact ⟨_, red.step.bnot, red.step.cons_bnot⟩
id └───────────┘ └────────────────┘
src └────────┘ └────────┘ └──┘ └───┘ └────┘ └─┘└───────────┘└┘└────────────────┘└┘
typ └────────┘ └────────┘ └──┘ └───┘ └────┘ └─┘└───────────┘└┘└────────────────┘└┘
doc └────────┘ └────────┘ └──┘ └───┘ └────┘ └─┘ └┘ └┘
txt └────────┘ └────────┘ └──┘ └───┘ └────┘ └─┘ └┘ └┘
par └────────┘ └────────┘ └──┘ └───┘ └────┘ └─┘ └┘ └┘
pid ┴ └─┘ └┘ ┴┴
st └─────────────────────────────────────────────────────────────────────────────────┘
112 | ((x3,b3)::(x4,b4)::tl) _ [] _ _ _ _ _ H :=
id ┴ └┘┴ └┘ └┘
src ┴ └┘┴ └┘ └┘
typ ┴ └┘┴ └┘ └┘
113 by injections; subst_vars; simp; right; exact ⟨_, red.step.cons_bnot, red.step.bnot⟩
id └────────────────┘ └───────────┘
src └────────┘ └────────┘ └──┘ └───┘ └────┘ └─┘└────────────────┘└┘└───────────┘└┘
typ └────────┘ └────────┘ └──┘ └───┘ └────┘ └─┘└────────────────┘└┘└───────────┘└┘
doc └────────┘ └────────┘ └──┘ └───┘ └────┘ └─┘ └┘ └┘
txt └────────┘ └────────┘ └──┘ └───┘ └────┘ └─┘ └┘ └┘
par └────────┘ └────────┘ └──┘ └───┘ └────┘ └─┘ └┘ └┘
pid ┴ └─┘ └┘ ┴┴
st └─────────────────────────────────────────────────────────────────────────────────┘
114 | ((x3,b3)::tl) _ ((x4,b4)::tl2) _ _ _ _ _ H :=
id ┴ └┘ ┴ └┘ ┴
src ┴ └┘ ┴ └┘
typ ┴ └┘ ┴ └┘ ┴
115 let ⟨H1, H2⟩ := list.cons.inj H in
id └─┘ └┘ └───────────┘
src └───────────┘
typ └─┘ └┘ └───────────┘
116 match step.diamond_aux H2 with
id └──────────────┘
typ └──────────────┘
117 | or.inl H3 := or.inl $ by simp [H1, H3]
id └────┘ └────┘ └┘ └┘
src └────┘ └────┘ └────┘ └┘ └─
typ └────┘ └────┘ └────┘└┘└┘└┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └──────────────
118 | or.inr ⟨L₅, H3, H4⟩ := or.inr
id └────┘ └┘ └────┘
src ───┘ └────┘ └────┘
typ ───┘ └────┘ └┘ └────┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘
119 ⟨_, step.cons H3, by simpa [H1] using step.cons H4⟩
id └───────┘ └┘ └───────┘ └┘
src └───────┘ └─────┘ └──────┘└───────┘┴
typ └───────┘ └─────┘└┘└──────┘└───────┘┴└┘
doc └─────┘ └──────┘ ┴
txt └─────┘ └──────┘ ┴
par └─────┘ └──────┘ ┴
pid ┴┴ ┴┴└────┘ ┴
st └────────────────────────────┘
120 end
121
122 theorem step.diamond : ∀ {L₁ L₂ L₃ L₄ : list (α × bool)},
id ┴ └──┘ ┴ ┴ └──┘
src └──┘ ┴ └──┘
typ ┴ └──┘ ┴ ┴ └──┘
123 red.step L₁ L₃ → red.step L₂ L₄ → L₁ = L₂ →
id └──────┘ └┘ └┘ └──────┘ └┘ └┘ └┘ ┴ └┘
src └──────┘ └──────┘ ┴
typ └──────┘ └┘ └┘ └──────┘ └┘ └┘ └┘ ┴ └┘
doc └──────┘ └──────┘
124 L₃ = L₄ ∨ ∃ L₅, red.step L₃ L₅ ∧ red.step L₄ L₅
id └┘ ┴ └┘ ┴ ┴ └┘┴ └──────┘ └┘ └┘ ┴ └──────┘ └┘ └┘
src ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘
typ └┘ ┴ └┘ ┴ ┴ └┘┴ └──────┘ └┘ └┘ ┴ └──────┘ └┘ └┘
doc └──────┘ └──────┘
125 | _ _ _ _ red.step.bnot red.step.bnot H := step.diamond_aux H
id └───────────┘ ┴ └──────────────┘
src └───────────┘ └──────────────┘
typ └───────────┘ ┴ └──────────────┘
126
127 lemma step.to_red : step L₁ L₂ → red L₁ L₂ :=
id └──┘ └┘ └┘ └─┘ └┘ └┘
src └──┘ └─┘
typ └──┘ └┘ └┘ └─┘ └┘ └┘
doc └──┘ └─┘
128 refl_trans_gen.single
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
129
130 /-- Church-Rosser theorem for word reduction: If `w1 w2 w3` are words such that `w1` reduces to `w2`
131 and `w3` respectively, then there is a word `w4` such that `w2` and `w3` reduce to `w4` respectively. -/
132 theorem church_rosser : red L₁ L₂ → red L₁ L₃ → join red L₂ L₃ :=
id └─┘ └┘ └┘ └─┘ └┘ └┘ └──┘ └─┘ └┘ └┘
src └─┘ └─┘ └──┘ └─┘
typ └─┘ └┘ └┘ └─┘ └┘ └┘ └──┘ └─┘ └┘ └┘
doc └─┘ └─┘ └─┘
133 relation.church_rosser (assume a b c hab hac,
id └────────────────────┘ ┴ ┴ ┴ └─┘ └─┘
src └────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ └─┘ └─┘
134 match b, c, red.step.diamond hab hac rfl with
id ┴ ┴ └──────────────┘ └─┘ └─┘ └─┘
src └──────────────┘ └─┘
typ ┴ ┴ └──────────────┘ └─┘ └─┘ └─┘
135 | b, _, or.inl rfl := ⟨b, by refl, by refl⟩
id ┴ └────┘ └─┘
src └────┘ └─┘ └──┘ └──┘
typ ┴ └────┘ └─┘ └──┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st └───┘ └───┘
136 | b, c, or.inr ⟨d, hbd, hcd⟩ := ⟨d, refl_gen.single hbd, hcd.to_red⟩
id └────┘ ┴ └─┘ └─┘ └─────────────┘ └─────┘
src └────┘ └─────────────┘ └─────┘
typ └────┘ ┴ └─┘ └─┘ └─────────────┘ └─────┘
137 end)
138
139 lemma cons_cons {p} : red L₁ L₂ → red (p :: L₁) (p :: L₂) :=
id └─┘ └┘ └┘ └─┘ ┴ └┘ └┘ ┴ └┘ └┘
src └─┘ └─┘ └┘ └┘
typ └─┘ └┘ └┘ └─┘ ┴ └┘ └┘ ┴ └┘ └┘
doc └─┘ └─┘
140 refl_trans_gen_lift (list.cons p) (assume a b, step.cons)
id └─────────────────┘ └───────┘ ┴ ┴ ┴ └───────┘
src └─────────────────┘ └───────┘ └───────┘
typ └─────────────────┘ └───────┘ ┴ ┴ ┴ └───────┘
141
142 lemma cons_cons_iff (p) : red (p :: L₁) (p :: L₂) ↔ red L₁ L₂ :=
id └─┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └─┘ └┘ └┘
src └─┘ └┘ └┘ ┴ └─┘
typ └─┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └─┘ └┘ └┘
doc └─┘ └─┘
143 iff.intro
id └───────┘
src └───────┘
typ └───────┘
144 begin
st └─────
145 generalize eq₁ : (p :: L₁ : list _) = LL₁,
id ┴ └┘ └──┘
src └───────────────┘ ┴ ┴ └─┘└──┘└──┘ ┴
typ └───────────────┘ ┴┴ ┴└┘└─┘└──┘└──┘ ┴
doc └───────────────┘ ┴ ┴ └─┘ └──┘ ┴
txt └───────────────┘ ┴ ┴ └─┘ └──┘ ┴
par └───────────────┘ ┴ ┴ └─┘ └──┘ ┴
pid └──┘└┘┴ ┴ ┴ └─┘ └──┘ ┴
st ────────────────────────────────────────────┘└─
146 generalize eq₂ : (p :: L₂ : list _) = LL₂,
id ┴ └┘ └──┘
src └───────────────┘ ┴ ┴ └─┘└──┘└──┘ ┴
typ └───────────────┘ ┴┴ ┴└┘└─┘└──┘└──┘ ┴
doc └───────────────┘ ┴ ┴ └─┘ └──┘ ┴
txt └───────────────┘ ┴ ┴ └─┘ └──┘ ┴
par └───────────────┘ ┴ ┴ └─┘ └──┘ ┴
pid └──┘└┘┴ ┴ ┴ └─┘ └──┘ ┴
st ────────────────────────────────────────────┘└─
147 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
148 induction h using relation.refl_trans_gen.head_induction_on
id ┴
src └────────┘ └────────────────────────────────────────────────
typ └────────┘┴└────────────────────────────────────────────────
doc └────────┘ └────────────────────────────────────────────────
txt └────────┘ └────────────────────────────────────────────────
par └────────┘ └────────────────────────────────────────────────
pid ┴ └──────────────────────────────────────────────┘└
st ────────────────────────────────────────────────────────────────
149 with L₁ L₂ h₁₂ h ih
src ──────────────────────────
typ ──────────────────────────
doc ──────────────────────────
txt ──────────────────────────
par ──────────────────────────
pid ────────────────────────┘└
st ──────────────────────────
150 generalizing L₁ L₂,
src ───────────────────────┘
typ ───────────────────────┘
doc ───────────────────────┘
txt ───────────────────────┘
par ───────────────────────┘
pid ───────────────────────┘
st ───────────────────────┘└─
151 { subst_vars, cases eq₂, constructor },
id └─┘
src └────────┘ └────┘ └──────────┘
typ └────────┘ └────┘└─┘ └──────────┘
doc └────────┘ └────┘ └──────────┘
txt └────────┘ └────┘ └──────────┘
par └────────┘ └────┘ └──────────┘
pid ┴ ┴
st ─────┘└────────┘└─────────┘└────────────┘└┘└
152 { subst_vars,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
st ───────────────┘└─
153 cases p with a b,
id ┴
src └────┘ └───────┘
typ └────┘┴└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ─────────────────────┘└─
154 rw [step.cons_left_iff] at h₁₂,
id └────────────────┘
src └──┘└────────────────┘└──────┘
typ └──┘└────────────────┘└──────┘
doc └──┘ └──────┘
txt └──┘ └──────┘
par └──┘ └──────┘
pid └┘ ┴└─────┘
st ───────────────────────────┘┴└─────┘└─
155 rcases h₁₂ with ⟨L, h₁₂, rfl⟩ | rfl,
id └─┘
src └─────┘ └───────────────────────┘
typ └─────┘└─┘└───────────────────────┘
doc └─────┘ └───────────────────────┘
txt └─────┘ └───────────────────────┘
par └─────┘ └───────────────────────┘
pid ┴ └───────────────────────┘
st ────────────────────────────────────────┘└─
156 { exact (ih rfl rfl).head h₁₂ },
id └┘ └─┘ └─┘
src └────┘ ┴ ┴└─┘└─────┘ ┴
typ └────┘ └┘┴ ┴└─┘└─────┘└─┘┴
doc └────┘ ┴ ┴ └─────┘ ┴
txt └────┘ ┴ ┴ └─────┘ ┴
par └────┘ ┴ ┴ └─────┘ ┴
pid ┴ ┴ ┴ └─────┘ ┴
st ───────┘└──────────────────────────┘└┘└
157 { exact (cons_cons h).tail step.cons_bnot_rev } }
id └───────┘ ┴ └────────────────┘
src └────┘ └───────┘┴ └─────┘└────────────────┘┴
typ └────┘ └───────┘┴┴└─────┘└────────────────┘┴
doc └────┘ ┴ └─────┘ ┴
txt └────┘ ┴ └─────┘ ┴
par └────┘ ┴ └─────┘ ┴
pid ┴ ┴ └─────┘ ┴
st ───────────────────────────────────────────────────┘└───
158 end
st ────┘
159 cons_cons
id └───────┘
src └───────┘
typ └───────┘
160
161 lemma append_append_left_iff : ∀L, red (L ++ L₁) (L ++ L₂) ↔ red L₁ L₂
id ┴ └─┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └─┘ └┘ └┘
src └─┘ └┘ └┘ ┴ └─┘
typ ┴ └─┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ └─┘ └┘ └┘
doc └─┘ └─┘
162 | [] := iff.rfl
id └┘ └─────┘
src └┘ └─────┘
typ └┘ └─────┘
163 | (p :: L) := by simp [append_append_left_iff L, cons_cons_iff]
id └┘ └────────────────────┘ ┴ └───────────┘
src └┘ └────┘ ┴ └┘└───────────┘└─
typ └┘ └────┘└────────────────────┘┴┴└┘└───────────┘└─
doc └────┘ ┴ └┘ └─
txt └────┘ ┴ └┘ └─
par └────┘ ┴ └┘ └─
pid ┴┴ ┴ └┘ ┴└
st └───────────────────────────────────────────────
164
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
165 lemma append_append (h₁ : red L₁ L₃) (h₂ : red L₂ L₄) : red (L₁ ++ L₂) (L₃ ++ L₄) :=
id └─┘ └┘ └┘ └─┘ └┘ └┘ └─┘ └┘ └┘ └┘ └┘ └┘ └┘
src └─┘ └─┘ └─┘ └┘ └┘
typ └─┘ └┘ └┘ └─┘ └┘ └┘ └─┘ └┘ └┘ └┘ └┘ └┘ └┘
doc └─┘ └─┘ └─┘
166 (refl_trans_gen_lift (λL, L ++ L₂) (assume a b, step.append_right) h₁).trans
id └─────────────────┘ ┴ ┴ └┘ └┘ ┴ ┴ └───────────────┘ └┘ └───┘
src └─────────────────┘ └┘ └───────────────┘ └───┘
typ └─────────────────┘ ┴ ┴ └┘ └┘ ┴ ┴ └───────────────┘ └┘ └───┘
167 ((append_append_left_iff _).2 h₂)
id └────────────────────┘ ┴ └┘
src └────────────────────┘ ┴
typ └────────────────────┘ ┴ └┘
168
169 lemma to_append_iff : red L (L₁ ++ L₂) ↔ (∃L₃ L₄, L = L₃ ++ L₄ ∧ red L₃ L₁ ∧ red L₄ L₂) :=
id └─┘ ┴ └┘ └┘ └┘ ┴ ┴└┘ └┘┴ ┴ ┴ └┘ └┘ └┘ ┴ └─┘ └┘ └┘ ┴ └─┘ └┘ └┘
src └─┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ └┘ └┘ └┘ ┴ ┴└┘ └┘┴ ┴ ┴ └┘ └┘ └┘ ┴ └─┘ └┘ └┘ ┴ └─┘ └┘ └┘
doc └─┘ └─┘ └─┘
170 iff.intro
id └───────┘
src └───────┘
typ └───────┘
171 begin
st └─────
172 generalize eq : L₁ ++ L₂ = L₁₂,
id └┘ └┘ └┘
src └──────────────┘ ┴└┘┴ ┴ ┴
typ └──────────────┘└┘┴└┘┴└┘┴ ┴
doc └──────────────┘ ┴ ┴ ┴ ┴
txt └──────────────┘ ┴ ┴ ┴ ┴
par └──────────────┘ ┴ ┴ ┴ ┴
pid └─┘└┘┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────┘└─
173 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
174 induction h with L' L₁₂ hLL' h ih generalizing L₁ L₂,
id ┴
src └────────┘ └───────────────────────────────────────┘
typ └────────┘┴└───────────────────────────────────────┘
doc └────────┘ └───────────────────────────────────────┘
txt └────────┘ └───────────────────────────────────────┘
par └────────┘ └───────────────────────────────────────┘
pid ┴ ┴└───────────────────┘└─────────────────┘
st ───────────────────────────────────────────────────────┘└─
175 { exact ⟨_, _, eq.symm, by refl, by refl⟩ },
id └─────┘
src └────┘ └────┘└─────┘└┘ ┴└──┘└┘ ┴└──┘└┘
typ └────┘ └────┘└─────┘└┘ ┴└──┘└┘ ┴└──┘└┘
doc └────┘ └────┘ └┘ ┴└──┘└┘ ┴└──┘└┘
txt └────┘ └────┘ └┘ ┴└──┘└┘ ┴└──┘└┘
par └────┘ └────┘ └┘ ┴└──┘└┘ ┴└──┘└┘
pid ┴ └────┘ └┘ └─────┘ └────┘┴
st ─────┘└──────────────────────┘└───┘└──┘└───┘└┘└┘└
176 { cases h with s e a b,
id ┴
src └────┘ └───────────┘
typ └────┘┴└───────────┘
doc └────┘ └───────────┘
txt └────┘ └───────────┘
par └────┘ └───────────┘
pid ┴ └───────────┘
st ─────────────────────────┘└─
177 rcases list.append_eq_append_iff.1 eq with ⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩,
id └───────────────────────┘ └┘
src └─────┘└───────────────────────┘└─┘└┘└───────────────────────────────────┘
typ └─────┘└───────────────────────┘└─┘└┘└───────────────────────────────────┘
doc └─────┘ └─┘ └───────────────────────────────────┘
txt └─────┘ └─┘ └───────────────────────────────────┘
par └─────┘ └─┘ └───────────────────────────────────┘
pid ┴ └─┘ └───────────────────────────────────┘
st ───────────────────────────────────────────────────────────────────────────────┘└─
178 { have : L₁ ++ (s' ++ ((a, b) :: (a, bnot b) :: e)) = (L₁ ++ s') ++ ((a, b) :: (a, bnot b) :: e),
id └┘ └┘ ┴┴ └──┘ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘ ┴┴ └┘└──┘┴ └┘ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ └┘┴ ┴└┘└┘ ┴ └┘ └┘ ┴┴┴└┘└──┘┴┴└┘ ┴┴┴
doc └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴
st ───────┘└────────────────────────────────────────────────────────────────────────────────────────────┘└─
179 { simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ─────────┘└───┘└┘└
180 rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩,
id └┘ └──┘
src └─────┘ ┴ └─────────────────────────┘
typ └─────┘└┘┴└──┘└─────────────────────────┘
doc └─────┘ ┴ └─────────────────────────┘
txt └─────┘ ┴ └─────────────────────────┘
par └─────┘ ┴ └─────────────────────────┘
pid ┴ ┴ └─────────────────────────┘
st ────────────────────────────────────────────────┘└─
181 exact ⟨w₁, w₂, rfl, h₁, h₂.tail step.bnot⟩ },
id └┘ └┘ └─┘ └┘ └─────┘ └───────┘
src └────┘ └┘ └┘└─┘└┘ └┘└─────┘┴└───────┘└┘
typ └────┘ └┘└┘└┘└┘└─┘└┘└┘└┘└─────┘┴└───────┘└┘
doc └────┘ └┘ └┘ └┘ └┘ ┴ └┘
txt └────┘ └┘ └┘ └┘ └┘ ┴ └┘
par └────┘ └┘ └┘ └┘ └┘ ┴ └┘
pid ┴ └┘ └┘ └┘ └┘ ┴ ┴┴
st ──────────────────────────────────────────────────┘└┘└
182 { have : (s ++ ((a, b) :: (a, bnot b) :: e')) ++ L₂ = s ++ ((a, b) :: (a, bnot b) :: (e' ++ L₂)),
id ┴ ┴┴ └──┘ ┴ └┘ └┘
src └─────┘ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴┴ └┘└──┘┴ └┘ ┴ ┴ ┴ └┘
typ └─────┘ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴┴┴ ┴ └┘ └┘ ┴┴┴└┘└──┘┴┴└┘ ┴ └┘┴ ┴└┘└┘
doc └─────┘ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘
txt └─────┘ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
183 { simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ─────────┘└───┘└┘└
184 rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩,
id └┘ └──┘
src └─────┘ ┴ └─────────────────────────┘
typ └─────┘└┘┴└──┘└─────────────────────────┘
doc └─────┘ ┴ └─────────────────────────┘
txt └─────┘ ┴ └─────────────────────────┘
par └─────┘ ┴ └─────────────────────────┘
pid ┴ ┴ └─────────────────────────┘
st ────────────────────────────────────────────────┘└─
185 exact ⟨w₁, w₂, rfl, h₁.tail step.bnot, h₂⟩ }, }
id └┘ └┘ └─┘ └─────┘ └───────┘ └┘
src └────┘ └┘ └┘└─┘└┘└─────┘┴└───────┘└┘ └┘
typ └────┘ └┘└┘└┘└┘└─┘└┘└─────┘┴└───────┘└┘└┘└┘
doc └────┘ └┘ └┘ └┘ ┴ └┘ └┘
txt └────┘ └┘ └┘ └┘ ┴ └┘ └┘
par └────┘ └┘ └┘ └┘ ┴ └┘ └┘
pid ┴ └┘ └┘ └┘ ┴ └┘ ┴┴
st ──────────────────────────────────────────────────┘└────
186 end
st ────┘
187 (assume ⟨L₃, L₄, eq, h₃, h₄⟩, eq.symm ▸ append_append h₃ h₄)
id ┴ └┘ └┘ └┘ └───┘ ┴ └───────────┘
src └┘ └───┘ ┴ └───────────┘
typ ┴ └┘ └┘ └┘ └───┘ ┴ └───────────┘
188
189 /-- The empty word `[]` only reduces to itself. -/
190 theorem nil_iff : red [] L ↔ L = [] :=
id └─┘ └┘ ┴ ┴ ┴ ┴ └┘
src └─┘ └┘ ┴ ┴ └┘
typ └─┘ └┘ ┴ ┴ ┴ ┴ └┘
doc └─┘
191 refl_trans_gen_iff_eq (assume l, red.not_step_nil)
id └───────────────────┘ ┴ └──────────────┘
src └───────────────────┘ └──────────────┘
typ └───────────────────┘ ┴ └──────────────┘
192
193 /-- A letter only reduces to itself. -/
194 theorem singleton_iff {x} : red [x] L₁ ↔ L₁ = [x] :=
id └─┘ ┴┴┴ └┘ ┴ └┘ ┴ ┴┴┴
src └─┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴┴┴ └┘ ┴ └┘ ┴ ┴┴┴
doc └─┘
195 refl_trans_gen_iff_eq (assume l, not_step_singleton)
id └───────────────────┘ ┴ └────────────────┘
src └───────────────────┘ └────────────────┘
typ └───────────────────┘ ┴ └────────────────┘
196
197 /-- If `x` is a letter and `w` is a word such that `xw` reduces to the empty word, then `w` reduces
198 to `x⁻¹` -/
199 theorem cons_nil_iff_singleton {x b} : red ((x, b) :: L) [] ↔ red L [(x, bnot b)] :=
id └─┘ ┴┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴┴┴ └──┘ ┴ ┴
src └─┘ ┴ └┘ └┘ ┴ └─┘ ┴┴ └──┘ ┴
typ └─┘ ┴┴ ┴ └┘ ┴ └┘ ┴ └─┘ ┴ ┴┴┴ └──┘ ┴ ┴
doc └─┘ └─┘
200 iff.intro
id └───────┘
src └───────┘
typ └───────┘
201 (assume h,
id ┴
typ ┴
202 have h₁ : red ((x, bnot b) :: (x, b) :: L) [(x, bnot b)], from cons_cons h,
id └─┘ ┴┴ └──┘ ┴ └┘ ┴┴ ┴ └┘ ┴ ┴┴┴ └──┘ ┴ ┴ └───────┘ ┴
src └─┘ ┴ └──┘ └┘ ┴ └┘ ┴┴ └──┘ ┴ └───────┘
typ └─┘ ┴┴ └──┘ ┴ └┘ ┴┴ ┴ └┘ ┴ ┴┴┴ └──┘ ┴ ┴ └───────┘ ┴
doc └─┘
203 have h₂ : red ((x, bnot b) :: (x, b) :: L) L, from refl_trans_gen.single step.cons_bnot_rev,
id └─┘ ┴┴ └──┘ ┴ └┘ ┴┴ ┴ └┘ ┴ ┴ └───────────────────┘ └────────────────┘
src └─┘ ┴ └──┘ └┘ ┴ └┘ └───────────────────┘ └────────────────┘
typ └─┘ ┴┴ └──┘ ┴ └┘ ┴┴ ┴ └┘ ┴ ┴ └───────────────────┘ └────────────────┘
doc └─┘
204 let ⟨L', h₁, h₂⟩ := church_rosser h₁ h₂ in
id └─┘ └───────────┘ └┘ └┘
src └───────────┘
typ └─┘ └───────────┘ └┘ └┘
doc └───────────┘
205 by rw [singleton_iff] at h₁; subst L'; assumption)
id └───────────┘ └┘
src └──┘└───────────┘└─────┘ └────┘ └────────┘
typ └──┘└───────────┘└─────┘ └────┘└┘ └────────┘
doc └──┘└───────────┘└─────┘ └────┘ └────────┘
txt └──┘ └─────┘ └────┘ └────────┘
par └──┘ └─────┘ └────┘ └────────┘
pid └┘ ┴└────┘ ┴
st └────────────────┘┴└──────────────────────────┘
206 (assume h, (cons_cons h).tail step.cons_bnot)
id ┴ └───────┘ ┴ └──┘ └────────────┘
src └───────┘ └──┘ └────────────┘
typ ┴ └───────┘ ┴ └──┘ └────────────┘
207
208 theorem red_iff_irreducible {x1 b1 x2 b2} (h : (x1, b1) ≠ (x2, b2)) :
id ┴└┘ └┘ ┴ ┴└┘ └┘
src ┴ ┴ ┴
typ ┴└┘ └┘ ┴ ┴└┘ └┘
209 red [(x1, bnot b1), (x2, b2)] L ↔ L = [(x1, bnot b1), (x2, b2)] :=
id └─┘ ┴┴└┘ └──┘ └┘ ┴ ┴└┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴└┘ └──┘ └┘ ┴ ┴└┘ └┘ ┴
src └─┘ ┴┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴┴ └──┘ ┴ ┴ ┴
typ └─┘ ┴┴└┘ └──┘ └┘ ┴ ┴└┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴┴└┘ └──┘ └┘ ┴ ┴└┘ └┘ ┴
doc └─┘
210 begin
st └─────
211 apply refl_trans_gen_iff_eq,
id └───────────────────┘
src └────┘└───────────────────┘
typ └────┘└───────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────┘└─
212 generalize eq : [(x1, bnot b1), (x2, b2)] = L',
id ┴ └┘ └──┘ └┘ ┴ ┴└┘ └┘ ┴
src └──────────────┘┴ └┘└──┘┴ ┴┴┴┴ └┘ ┴┴┴ ┴
typ └──────────────┘┴ └┘└┘└──┘┴└┘┴┴┴┴└┘└┘└┘┴┴┴ ┴
doc └──────────────┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
txt └──────────────┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
par └──────────────┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
pid └─┘└┘┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
st ───────────────────────────────────────────────┘└─
213 assume L h',
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────┘└─
214 cases h',
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────┘└─
215 simp [list.cons_eq_append_iff, list.nil_eq_append_iff] at eq,
id └─────────────────────┘ └────────────────────┘
src └────┘└─────────────────────┘└┘└────────────────────┘└─────┘
typ └────┘└─────────────────────┘└┘└────────────────────┘└─────┘
doc └────┘ └┘ └─────┘
txt └────┘ └┘ └─────┘
par └────┘ └┘ └─────┘
pid ┴┴ └┘ ┴┴└───┘
st ─────────────────────────────────────────────────────────────┘└─
216 rcases eq with ⟨rfl, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl⟩, subst_vars,
id └┘
src └─────┘└┘└──────────────────────────────────────┘ └────────┘
typ └─────┘└┘└──────────────────────────────────────┘ └────────┘
doc └─────┘ └──────────────────────────────────────┘ └────────┘
txt └─────┘ └──────────────────────────────────────┘ └────────┘
par └─────┘ └──────────────────────────────────────┘ └────────┘
pid ┴ └──────────────────────────────────────┘
st ──────────────────────────────────────────────────┘└─────────────
217 simp at h,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└──┘
st ──────────┘└─
218 contradiction
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───────────────┘
219 end
st └─┘
220
221 /-- If `x` and `y` are distinct letters and `w₁ w₂` are words such that `xw₁` reduces to `yw₂`, then
222 `w₁` reduces to `x⁻¹yw₂`. -/
223 theorem inv_of_red_of_ne {x1 b1 x2 b2}
224 (H1 : (x1, b1) ≠ (x2, b2))
id ┴└┘ └┘ ┴ ┴└┘ └┘
src ┴ ┴ ┴
typ ┴└┘ └┘ ┴ ┴└┘ └┘
225 (H2 : red ((x1, b1) :: L₁) ((x2, b2) :: L₂)) :
id └─┘ ┴└┘ └┘ └┘ └┘ ┴└┘ └┘ └┘ └┘
src └─┘ ┴ └┘ ┴ └┘
typ └─┘ ┴└┘ └┘ └┘ └┘ ┴└┘ └┘ └┘ └┘
doc └─┘
226 red L₁ ((x1, bnot b1) :: (x2, b2) :: L₂) :=
id └─┘ └┘ ┴└┘ └──┘ └┘ └┘ ┴└┘ └┘ └┘ └┘
src └─┘ ┴ └──┘ └┘ ┴ └┘
typ └─┘ └┘ ┴└┘ └──┘ └┘ └┘ ┴└┘ └┘ └┘ └┘
doc └─┘
227 begin
st └─────
228 have : red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂), from H2,
id └─┘ └┘ └┘ └┘ ┴┴└┘ └┘ ┴ └┘ └┘ └┘
src └─────┘└─┘┴ └┘ └┘ ┴ └┘ ┴┴ └┘ ┴┴┴└┘┴ ┴ └───┘
typ └─────┘└─┘┴ └┘└┘└┘└┘ ┴└┘└┘ ┴┴└┘└┘└┘┴┴┴└┘┴└┘┴ └───┘└┘
doc └─────┘└─┘┴ └┘ └┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └───┘
txt └─────┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └───┘
par └─────┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └───┘
pid └───┘└┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └───┘
st ───────────────────────────────────────────────┘└───────┘└─
229 rcases to_append_iff.1 this with ⟨_ | ⟨p, L₃⟩, L₄, eq, h₁, h₂⟩,
id └───────────┘ └──┘
src └─────┘└───────────┘└─┘ └─────────────────────────────────┘
typ └─────┘└───────────┘└─┘└──┘└─────────────────────────────────┘
doc └─────┘ └─┘ └─────────────────────────────────┘
txt └─────┘ └─┘ └─────────────────────────────────┘
par └─────┘ └─┘ └─────────────────────────────────┘
pid ┴ └─┘ └─────────────────────────────────┘
st ───────────────────────────────────────────────────────────────┘└─
230 { simp [nil_iff] at h₁, contradiction },
id └─────┘
src └────┘└─────┘└─────┘ └────────────┘
typ └────┘└─────┘└─────┘ └────────────┘
doc └────┘└─────┘└─────┘ └────────────┘
txt └────┘ └─────┘ └────────────┘
par └────┘ └─────┘ └────────────┘
pid ┴┴ ┴┴└───┘ ┴
st ───┘└──────────────────┘└──────────────┘└┘└
231 { cases eq,
id └┘
src └────┘└┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────┘└─
232 show red (L₃ ++ L₄) ([(x1, bnot b1), (x2, b2)] ++ L₂),
id └─┘ └┘ └┘ ┴ └┘ └──┘ └┘ ┴ ┴└┘ └┘ ┴ └┘
src └───┘└─┘┴ ┴ ┴ └┘ ┴ └┘└──┘┴ ┴┴┴┴ └┘ ┴┴┴ ┴ ┴
typ └───┘└─┘┴ └┘┴ ┴└┘└┘ ┴ └┘└┘└──┘┴└┘┴┴┴┴└┘└┘└┘┴┴┴ ┴└┘┴
doc └───┘└─┘┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
txt └───┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────┘└─
233 apply append_append _ h₂,
id └───────────┘ └┘
src └────┘└───────────┘└─┘
typ └────┘└───────────┘└─┘└┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ───────────────────────────┘└─
234 have h₁ : red ((x1, bnot b1) :: (x1, b1) :: L₃) [(x1, bnot b1), (x2, b2)],
id └─┘ └┘ ┴ └┘ └──┘ └┘ ┴ ┴└┘ └┘ ┴
src └────────┘└─┘┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘┴ └┘└──┘┴ ┴┴┴┴ └┘ ┴┴
typ └────────┘└─┘┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴└┘└┘┴ └┘└┘└──┘┴└┘┴┴┴┴└┘└┘└┘┴┴
doc └────────┘└─┘┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴
txt └────────┘ ┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴
par └────────┘ ┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴
pid └─────┘└─┘ ┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────────────────────────────────┘└─
235 { exact cons_cons h₁ },
id └───────┘ └┘
src └────┘└───────┘┴ ┴
typ └────┘└───────┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────┘└─────────────────┘└┘└
236 have h₂ : red ((x1, bnot b1) :: (x1, b1) :: L₃) L₃,
id └─┘ └──┘ ┴└┘ └┘ └┘
src └────────┘└─┘┴ └┘└──┘┴ └┘ ┴┴ └┘ └┘ ┴ └┘
typ └────────┘└─┘┴ └┘└──┘┴ └┘ ┴┴└┘└┘└┘└┘ ┴ └┘└┘
doc └────────┘└─┘┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘
txt └────────┘ ┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘
par └────────┘ ┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘
pid └─────┘└─┘ ┴ └┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘
st ─────────────────────────────────────────────────────┘└─
237 { exact step.cons_bnot_rev.to_red },
id └───────────────────────┘
src └────┘└───────────────────────┘┴
typ └────┘└───────────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────┘└──────────────────────────────┘└┘└
238 rcases church_rosser h₁ h₂ with ⟨L', h₁, h₂⟩,
id └───────────┘ └┘ └┘
src └─────┘└───────────┘┴ ┴ └────────────────┘
typ └─────┘└───────────┘┴└┘┴└┘└────────────────┘
doc └─────┘└───────────┘┴ ┴ └────────────────┘
txt └─────┘ ┴ ┴ └────────────────┘
par └─────┘ ┴ ┴ └────────────────┘
pid ┴ ┴ ┴ └────────────────┘
st ───────────────────────────────────────────────┘└─
239 rw [red_iff_irreducible H1] at h₁,
id └─────────────────┘ └┘
src └──┘└─────────────────┘┴ └─────┘
typ └──┘└─────────────────┘┴└┘└─────┘
doc └──┘ ┴ └─────┘
txt └──┘ ┴ └─────┘
par └──┘ ┴ └─────┘
pid └┘ ┴ ┴└────┘
st ─────────────────────────────┘┴└────┘└─
240 rwa [h₁] at h₂ }
id └┘
src └───┘ └──────┘
typ └───┘└┘└──────┘
doc └───┘ └──────┘
txt └───┘ └──────┘
par └───┘ └──────┘
pid └┘ ┴└────┘┴
st ──────────┘┴└─────┘└─
241 end
st ──┘
242
243 theorem step.sublist (H : red.step L₁ L₂) : L₂ <+ L₁ :=
id └──────┘ └┘ └┘ └┘ └┘ └┘
src └──────┘ └┘
typ └──────┘ └┘ └┘ └┘ └┘ └┘
doc └──────┘
244 by cases H; simp; constructor; constructor; refl
id ┴
src └────┘ └──┘ └─────────┘ └─────────┘ └────
typ └────┘┴ └──┘ └─────────┘ └─────────┘ └────
doc └────┘ └──┘ └─────────┘ └─────────┘ └────
txt └────┘ └──┘ └─────────┘ └─────────┘ └────
par └────┘ └──┘ └─────────┘ └─────────┘ └────
pid ┴ └
st └──────────────────────────────────────────────
245
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
246 /-- If `w₁ w₂` are words such that `w₁` reduces to `w₂`, then `w₂` is a sublist of `w₁`. -/
247 theorem sublist : red L₁ L₂ → L₂ <+ L₁ :=
id └─┘ └┘ └┘ └┘ └┘ └┘
src └─┘ └┘
typ └─┘ └┘ └┘ └┘ └┘ └┘
doc └─┘
248 refl_trans_gen_of_transitive_reflexive
id └────────────────────────────────────┘
src └────────────────────────────────────┘
typ └────────────────────────────────────┘
249 (λl, list.sublist.refl l) (λa b c hab hbc, list.sublist.trans hbc hab) (λa b, red.step.sublist)
id ┴ └───────────────┘ ┴ ┴ ┴ ┴ └─┘ └─┘ └────────────────┘ └─┘ └─┘ ┴ ┴ └──────────────┘
src └───────────────┘ └────────────────┘ └──────────────┘
typ ┴ └───────────────┘ ┴ ┴ ┴ ┴ └─┘ └─┘ └────────────────┘ └─┘ └─┘ ┴ ┴ └──────────────┘
250
251 theorem sizeof_of_step : ∀ {L₁ L₂ : list (α × bool)}, step L₁ L₂ → L₂.sizeof < L₁.sizeof
id ┴ └──┘ ┴ ┴ └──┘ └──┘ └┘ └┘ └┘└─────┘ ┴ └┘└─────┘
src └──┘ ┴ └──┘ └──┘ └─────┘ ┴ └─────┘
typ ┴ └──┘ ┴ ┴ └──┘ └──┘ └┘ └┘ └┘└─────┘ ┴ └┘└─────┘
doc └──┘
252 | _ _ (@step.bnot _ L1 L2 x b) :=
id └───────┘
src └───────┘
typ └───────┘
253 begin
st └─────
254 induction L1 with hd tl ih,
id └┘
src └────────┘ └────────────┘
typ └────────┘└┘└────────────┘
doc └────────┘ └────────────┘
txt └────────┘ └────────────┘
par └────────┘ └────────────┘
pid ┴ ┴└───────────┘
st ─────────────────────────────┘└─
255 case list.nil
src └─────────────
typ └─────────────
doc └─────────────
txt └─────────────
par └─────────────
pid └───────┘└
st ──────────────────
256 { dsimp [list.sizeof],
id └─────────┘
src ─────┘└─────┘└─────────┘┴└─
typ ─────┘└─────┘└─────────┘┴└─
doc ─────┘└─────┘ ┴└─
txt ─────┘└─────┘ ┴└─
par ─────┘└─────┘ ┴└─
pid ───┘└───────┘ └──
st ────┘└──────────────────┘└─
257 have H : 1 + sizeof (x, b) + (1 + sizeof (x, bnot b) + list.sizeof L2)
id ┴
src ─────┘└─────────┘┴┴ ┴ └┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─
typ ─────┘└─────────┘┴┴ ┴ └┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─
doc ─────┘└─────────┘ ┴ ┴ └┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─
txt ─────┘└─────────┘ ┴ ┴ └┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─
par ─────┘└─────────┘ ┴ ┴ └┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─
pid ────────────────┘ ┴ ┴ └┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └─
st ─────────────────────────────────────────────────────────────────────────────
258 = (list.sizeof L2 + 1) + (sizeof (x, b) + sizeof (x, bnot b) + 1),
id ┴ └─────────┘ └┘ └────┘ ┴┴ └──┘ ┴
src ───────┘┴┴ └─────────┘┴ ┴ └──┘ ┴ ┴ └┘ └┘ ┴└────┘┴┴ └┘└──┘┴ └┘ └─┘└─
typ ───────┘┴┴ └─────────┘┴└┘┴ └──┘ ┴ ┴ └┘ └┘ ┴└────┘┴┴┴└┘└──┘┴┴└┘ └─┘└─
doc ───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ └─┘└─
txt ───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ └─┘└─
par ───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ └─┘└─
pid ───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ └────
st ────────────────────────────────────────────────────────────────────────┘└─
259 { ac_refl },
src ───────┘└──────┘└──
typ ───────┘└──────┘└──
doc ───────┘└──────┘└──
txt ───────┘└──────┘└──
par ───────┘└──────┘└──
pid ───────────────────
st ──────┘└───────┘┴└─
260 rw H,
id ┴
src ─────┘└─┘ └─
typ ─────┘└─┘┴└─
doc ─────┘└─┘ └─
txt ─────┘└─┘ └─
par ─────┘└─┘ └─
pid ────────┘ └─
st ─────────┘└─
261 exact nat.le_add_right _ _ },
id └──────────────┘
src ─────┘└────┘└──────────────┘└───┘┴
typ ─────┘└────┘└──────────────┘└───┘┴
doc ─────┘└────┘ └───┘┴
txt ─────┘└────┘ └───┘┴
par ─────┘└────┘ └───┘┴
pid ───────────┘ └────┘
st ────────────────────────────────┘└┘└
262 case list.cons
src └──────────────
typ └──────────────
doc └──────────────
txt └──────────────
par └──────────────
pid └────────┘└
st ───────────────────
263 { dsimp [list.sizeof],
id └─────────┘
src ─────┘└─────┘└─────────┘┴└─
typ ─────┘└─────┘└─────────┘┴└─
doc ─────┘└─────┘ ┴└─
txt ─────┘└─────┘ ┴└─
par ─────┘└─────┘ ┴└─
pid ───┘└───────┘ └──
st ────────────────────────┘└─
264 exact nat.add_lt_add_left ih _ }
id └─────────────────┘ └┘
src ─────┘└────┘└─────────────────┘┴ └─┘└─
typ ─────┘└────┘└─────────────────┘┴└┘└─┘└─
doc ─────┘└────┘ ┴ └─┘└─
txt ─────┘└────┘ ┴ └─┘└─
par ─────┘└────┘ ┴ └─┘└─
pid ───────────┘ ┴ └──┘└
st ────────────────────────────────────┘┴└
265 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
266
267 theorem length (h : red L₁ L₂) : ∃ n, L₁.length = L₂.length + 2 * n :=
id └─┘ └┘ └┘ ┴ ┴┴ └┘└─────┘ ┴ └┘└─────┘ ┴ ┴ ┴
src └─┘ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴
typ └─┘ └┘ └┘ ┴ ┴┴ └┘└─────┘ ┴ └┘└─────┘ ┴ ┴ ┴
doc └─┘
268 begin
st └─────
269 induction h with L₂ L₃ h₁₂ h₂₃ ih,
id ┴
src └────────┘ └────────────────────┘
typ └────────┘┴└────────────────────┘
doc └────────┘ └────────────────────┘
txt └────────┘ └────────────────────┘
par └────────┘ └────────────────────┘
pid ┴ ┴└───────────────────┘
st ──────────────────────────────────┘└─
270 { exact ⟨0, rfl⟩ },
id └─┘
src └────┘ └─┘└─┘└┘
typ └────┘ └─┘└─┘└┘
doc └────┘ └─┘ └┘
txt └────┘ └─┘ └┘
par └────┘ └─┘ └┘
pid ┴ └─┘ ┴┴
st ───┘└─────────────┘└┘└
271 { rcases ih with ⟨n, eq⟩,
id └┘
src └─────┘ └───────────┘
typ └─────┘└┘└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ─────────────────────────┘└─
272 existsi (1 + n),
id ┴ ┴
src └──────┘ └┘┴┴ ┴
typ └──────┘ └┘┴┴┴┴
doc └──────┘ └┘ ┴ ┴
txt └──────┘ └┘ ┴ ┴
par └──────┘ └┘ ┴ ┴
pid ┴ └┘ ┴ ┴
st ──────────────────┘└─
273 simp [mul_add, eq, (step.length h₂₃).symm] }
id └─────┘ └┘ └─────────┘ └─┘
src └────┘└─────┘└┘└┘└┘ └─────────┘┴ └──────┘
typ └────┘└─────┘└┘└┘└┘ └─────────┘┴└─┘└──────┘
doc └────┘ └┘ └┘ └─────────┘┴ └──────┘
txt └────┘ └┘ └┘ ┴ └──────┘
par └────┘ └┘ └┘ ┴ └──────┘
pid ┴┴ └┘ └┘ ┴ └─────┘┴
st ──────────────────────────────────────────────┘└─
274 end
st ──┘
275
276 theorem antisymm (h₁₂ : red L₁ L₂) : red L₂ L₁ → L₁ = L₂ :=
id └─┘ └┘ └┘ └─┘ └┘ └┘ └┘ ┴ └┘
src └─┘ └─┘ ┴
typ └─┘ └┘ └┘ └─┘ └┘ └┘ └┘ ┴ └┘
doc └─┘ └─┘
277 match L₁, h₁₂.cases_head with
id └┘ └─┘└─────────┘
src └─────────┘
typ └┘ └─┘└─────────┘
278 | _, or.inl rfl := assume h, rfl
id └────┘ └─┘ ┴ └─┘
src └────┘ └─┘ └─┘
typ └────┘ └─┘ ┴ └─┘
279 | L₁, or.inr ⟨L₃, h₁₃, h₃₂⟩ := assume h₂₁,
id └────┘ └┘ └─┘ └─┘
src └────┘
typ └────┘ └┘ └─┘ └─┘
280 let ⟨n, eq⟩ := length (h₃₂.trans h₂₁) in
id └─┘ ┴ └────┘ └────┘ └─┘
src └────┘ └────┘
typ └─┘ ┴ └────┘ └────┘ └─┘
281 have list.length L₃ + 0 = list.length L₃ + (2 * n + 2),
id └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ ┴
src └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ └─────────┘ ┴ ┴ ┴
282 by simpa [(step.length h₁₃).symm, add_comm, add_assoc] using eq,
id └─────────┘ └─┘ └──────┘ └───────┘ └┘
src └─────┘ └─────────┘┴ └──────┘└──────┘└┘└───────┘└──────┘└┘
typ └─────┘ └─────────┘┴└─┘└──────┘└──────┘└┘└───────┘└──────┘└┘
doc └─────┘ └─────────┘┴ └──────┘ └┘ └──────┘
txt └─────┘ ┴ └──────┘ └┘ └──────┘
par └─────┘ ┴ └──────┘ └┘ └──────┘
pid ┴┴ ┴ └──────┘ └┘ ┴┴└────┘
st └───────────────────────────────────────────────────────────┘
283 (nat.no_confusion $ nat.add_left_cancel this)
id └──────────────┘ └─────────────────┘ └──┘
src └──────────────┘ └─────────────────┘
typ └──────────────┘ └─────────────────┘ └──┘
284 end
285
286 end red
287
288 theorem equivalence_join_red : equivalence (join (@red α)) :=
id └─────────┘ └──┘ └─┘ ┴
src └─────────┘ └──┘ └─┘
typ └─────────┘ └──┘ └─┘ ┴
doc └─┘
289 equivalence_join_refl_trans_gen $ assume a b c hab hac,
id └─────────────────────────────┘ ┴ ┴ ┴ └─┘ └─┘
src └─────────────────────────────┘
typ └─────────────────────────────┘ ┴ ┴ ┴ └─┘ └─┘
290 (match b, c, red.step.diamond hab hac rfl with
id ┴ ┴ └──────────────┘ └─┘ └─┘ └─┘
src └──────────────┘ └─┘
typ ┴ ┴ └──────────────┘ └─┘ └─┘ └─┘
291 | b, _, or.inl rfl := ⟨b, by refl, by refl⟩
id ┴ └────┘ └─┘
src └────┘ └─┘ └──┘ └──┘
typ ┴ └────┘ └─┘ └──┘ └──┘
doc └──┘ └──┘
txt └──┘ └──┘
par └──┘ └──┘
st └───┘ └───┘
292 | b, c, or.inr ⟨d, hbd, hcd⟩ := ⟨d, refl_gen.single hbd, refl_trans_gen.single hcd⟩
id └────┘ ┴ └─┘ └─┘ └─────────────┘ └───────────────────┘
src └────┘ └─────────────┘ └───────────────────┘
typ └────┘ ┴ └─┘ └─┘ └─────────────┘ └───────────────────┘
293 end)
294
295 theorem join_red_of_step (h : red.step L₁ L₂) : join red L₁ L₂ :=
id └──────┘ └┘ └┘ └──┘ └─┘ └┘ └┘
src └──────┘ └──┘ └─┘
typ └──────┘ └┘ └┘ └──┘ └─┘ └┘ └┘
doc └──────┘ └─┘
296 join_of_single reflexive_refl_trans_gen h.to_red
id └────────────┘ └──────────────────────┘ ┴└─────┘
src └────────────┘ └──────────────────────┘ └─────┘
typ └────────────┘ └──────────────────────┘ ┴└─────┘
297
298 theorem eqv_gen_step_iff_join_red : eqv_gen red.step L₁ L₂ ↔ join red L₁ L₂ :=
id └─────┘ └──────┘ └┘ └┘ ┴ └──┘ └─┘ └┘ └┘
src └─────┘ └──────┘ ┴ └──┘ └─┘
typ └─────┘ └──────┘ └┘ └┘ ┴ └──┘ └─┘ └┘ └┘
doc └──────┘ └─┘
299 iff.intro
id └───────┘
src └───────┘
typ └───────┘
300 (assume h,
id ┴
typ ┴
301 have eqv_gen (join red) L₁ L₂ := eqv_gen_mono (assume a b, join_red_of_step) h,
id └─────┘ └──┘ └─┘ └┘ └┘ └──────────┘ ┴ ┴ └──────────────┘ ┴
src └─────┘ └──┘ └─┘ └──────────┘ └──────────────┘
typ └─────┘ └──┘ └─┘ └┘ └┘ └──────────┘ ┴ ┴ └──────────────┘ ┴
doc └─┘
302 (eqv_gen_iff_of_equivalence $ equivalence_join_red).1 this)
id └────────────────────────┘ └──────────────────┘ ┴ └──┘
src └────────────────────────┘ └──────────────────┘ ┴
typ └────────────────────────┘ └──────────────────┘ ┴ └──┘
303 (join_of_equivalence (eqv_gen.is_equivalence _) $ assume a b,
id └─────────────────┘ └────────────────────┘ ┴ ┴
src └─────────────────┘ └────────────────────┘
typ └─────────────────┘ └────────────────────┘ ┴ ┴
304 refl_trans_gen_of_equivalence (eqv_gen.is_equivalence _) eqv_gen.rel)
id └───────────────────────────┘ └────────────────────┘ └─────────┘
src └───────────────────────────┘ └────────────────────┘ └─────────┘
typ └───────────────────────────┘ └────────────────────┘ └─────────┘
305
306 end free_group
307
308 /-- The free group over a type, i.e. the words formed by the elements of the type and their formal
309 inverses, quotient by one step reduction. -/
310 def free_group (α : Type u) : Type u :=
311 quot $ @free_group.red.step α
id └──┘ └─────────────────┘ ┴
src └─────────────────┘
typ └──┘ └─────────────────┘ ┴
doc └─────────────────┘
312
313 namespace free_group
314
315 variables {α} {L L₁ L₂ L₃ L₄ : list (α × bool)}
id └──┘ ┴ └──┘
src └──┘ ┴ └──┘
typ └──┘ ┴ └──┘
316
317 def mk (L) : free_group α := quot.mk red.step L
id └────────┘ ┴ └─────┘ └──────┘ ┴
src └────────┘ └──────┘
typ └────────┘ ┴ └─────┘ └──────┘ ┴
doc └────────┘ └──────┘
318
319 @[simp] lemma quot_mk_eq_mk : quot.mk red.step L = mk L := rfl
id └─────┘ └──────┘ ┴ ┴ └┘ ┴ └─┘
src └──────┘ ┴ └┘ └─┘
typ └─────┘ └──────┘ ┴ ┴ └┘ ┴ └─┘
doc └──┘ └──────┘
320
321 @[simp] lemma quot_lift_mk (β : Type v) (f : list (α × bool) → β)
id └──┘ ┴ ┴ └──┘ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴ └──┘ ┴
doc └──┘
322 (H : ∀ L₁ L₂, red.step L₁ L₂ → f L₁ = f L₂) :
id └┘ └┘ └──────┘ └┘ └┘ ┴ └┘ ┴ ┴ └┘
src └──────┘ ┴
typ └┘ └┘ └──────┘ └┘ └┘ ┴ └┘ ┴ ┴ └┘
doc └──────┘
323 quot.lift f H (mk L) = f L := rfl
id └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
src └┘ ┴ └─┘
typ └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
324
325 @[simp] lemma quot_lift_on_mk (β : Type v) (f : list (α × bool) → β)
id └──┘ ┴ ┴ └──┘ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴ └──┘ ┴
doc └──┘
326 (H : ∀ L₁ L₂, red.step L₁ L₂ → f L₁ = f L₂) :
id └┘ └┘ └──────┘ └┘ └┘ ┴ └┘ ┴ ┴ └┘
src └──────┘ ┴
typ └┘ └┘ └──────┘ └┘ └┘ ┴ └┘ ┴ ┴ └┘
doc └──────┘
327 quot.lift_on (mk L) f H = f L := rfl
id └──────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └──────────┘ └┘ ┴ └─┘
typ └──────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
328
329 instance : has_one (free_group α) := ⟨mk []⟩
id └─────┘ └────────┘ ┴ └┘ └┘
src └─────┘ └────────┘ └┘ └┘
typ └─────┘ └────────┘ ┴ └┘ └┘
doc └────────┘
330 lemma one_eq_mk : (1 : free_group α) = mk [] := rfl
id └────────┘ ┴ ┴ └┘ └┘ └─┘
src └────────┘ ┴ └┘ └┘ └─┘
typ └────────┘ ┴ ┴ └┘ └┘ └─┘
doc └────────┘
331
332 instance : inhabited (free_group α) := ⟨1⟩
id └───────┘ └────────┘ ┴
src └───────┘ └────────┘
typ └───────┘ └────────┘ ┴
doc └────────┘
333
334 instance : has_mul (free_group α) :=
id └─────┘ └────────┘ ┴
src └─────┘ └────────┘
typ └─────┘ └────────┘ ┴
doc └────────┘
335 ⟨λ x y, quot.lift_on x
id ┴ ┴ └──────────┘ ┴
src └──────────┘
typ ┴ ┴ └──────────┘ ┴
336 (λ L₁, quot.lift_on y (λ L₂, mk $ L₁ ++ L₂) (λ L₂ L₃ H, quot.sound $ red.step.append_left H))
id └┘ └──────────┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └────────┘ └──────────────────┘ ┴
src └──────────┘ └┘ └┘ └────────┘ └──────────────────┘
typ └┘ └──────────┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘ └┘ ┴ └────────┘ └──────────────────┘ ┴
337 (λ L₁ L₂ H, quot.induction_on y $ λ L₃, quot.sound $ red.step.append_right H)⟩
id └┘ └┘ ┴ └───────────────┘ ┴ └┘ └────────┘ └───────────────────┘ ┴
src └───────────────┘ └────────┘ └───────────────────┘
typ └┘ └┘ ┴ └───────────────┘ ┴ └┘ └────────┘ └───────────────────┘ ┴
338 @[simp] lemma mul_mk : mk L₁ * mk L₂ = mk (L₁ ++ L₂) := rfl
id └┘ └┘ ┴ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └─┘
src └┘ ┴ └┘ ┴ └┘ └┘ └─┘
typ └┘ └┘ ┴ └┘ └┘ ┴ └┘ └┘ └┘ └┘ └─┘
doc └──┘
339
340 instance : has_inv (free_group α) :=
id └─────┘ └────────┘ ┴
src └─────┘ └────────┘
typ └─────┘ └────────┘ ┴
doc └────────┘
341 ⟨λx, quot.lift_on x (λ L, mk (L.map $ λ x : α × bool, (x.1, bnot x.2)).reverse)
id ┴ └──────────┘ ┴ ┴ └┘ ┴└──┘ ┴ ┴ └──┘ ┴┴┴ └──┘ ┴┴ └─────┘
src └──────────┘ └┘ └──┘ ┴ └──┘ ┴ ┴ └──┘ ┴ └─────┘
typ ┴ └──────────┘ ┴ ┴ └┘ ┴└──┘ ┴ ┴ └──┘ ┴┴┴ └──┘ ┴┴ └─────┘
342 (assume a b h, quot.sound $ by cases h; simp)⟩
id ┴ ┴ ┴ └────────┘ ┴
src └────────┘ └────┘ └──┘
typ ┴ ┴ ┴ └────────┘ └────┘┴ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st └────────────┘
343 @[simp] lemma inv_mk : (mk L)⁻¹ = mk (L.map $ λ x : α × bool, (x.1, bnot x.2)).reverse := rfl
id └┘ ┴ └┘ ┴ └┘ ┴└──┘ ┴ ┴ └──┘ ┴┴┴ └──┘ ┴┴ └─────┘ └─┘
src └┘ └┘ ┴ └┘ └──┘ ┴ └──┘ ┴ ┴ └──┘ ┴ └─────┘ └─┘
typ └┘ ┴ └┘ ┴ └┘ ┴└──┘ ┴ ┴ └──┘ ┴┴┴ └──┘ ┴┴ └─────┘ └─┘
doc └──┘
344
345 instance : group (free_group α) :=
id └───┘ └────────┘ ┴
src └───┘ └────────┘
typ └───┘ └────────┘ ┴
doc └────────┘
346 { mul := (*),
id ┴
src ┴
typ ┴
347 one := 1,
348 inv := has_inv.inv,
id └─────────┘
src └─────────┘
typ └─────────┘
349 mul_assoc := by rintros ⟨L₁⟩ ⟨L₂⟩ ⟨L₃⟩; simp,
src └────────────────────┘ └──┘
typ └────────────────────┘ └──┘
doc └────────────────────┘ └──┘
txt └────────────────────┘ └──┘
par └────────────────────┘ └──┘
pid └─────────────┘
st └───────────────────────────┘
350 one_mul := by rintros ⟨L⟩; refl,
src └─────────┘ └──┘
typ └─────────┘ └──┘
doc └─────────┘ └──┘
txt └─────────┘ └──┘
par └─────────┘ └──┘
pid └──┘
st └────────────────┘
351 mul_one := by rintros ⟨L⟩; simp [one_eq_mk],
id └───────┘
src └─────────┘ └────┘└───────┘┴
typ └─────────┘ └────┘└───────┘┴
doc └─────────┘ └────┘ ┴
txt └─────────┘ └────┘ ┴
par └─────────┘ └────┘ ┴
pid └──┘ ┴┴ ┴
st └────────────────────────────┘
352 mul_left_inv := by rintros ⟨L⟩; exact (list.rec_on L rfl $
id └─────────┘ ┴ └─┘
src └─────────┘ └────┘ └─────────┘┴ ┴└─┘┴ └
typ └─────────┘ └────┘ └─────────┘┴┴┴└─┘┴ └
doc └─────────┘ └────┘ ┴ ┴ ┴ └
txt └─────────┘ └────┘ ┴ ┴ ┴ └
par └─────────┘ └────┘ ┴ ┴ ┴ └
pid └──┘ ┴ ┴ ┴ ┴ └
st └────────────────────────────────────────
353 λ ⟨x, b⟩ tl ih, eq.trans (quot.sound $ by simp [one_eq_mk]) ih) }
id └──────┘ └────────┘ └───────┘
src ───┘ └┘ └┘ └───────┘└──────┘┴ └────────┘┴ ┴ ┴└────┘└───────┘┴└┘ └┘
typ ───┘ └┘ └┘ └───────┘└──────┘┴ └────────┘┴ ┴ ┴└────┘└───────┘┴└┘ └┘
doc ───┘ └┘ └┘ └───────┘ ┴ ┴ ┴ ┴└────┘ ┴└┘ └┘
txt ───┘ └┘ └┘ └───────┘ ┴ ┴ ┴ ┴└────┘ ┴└┘ └┘
par ───┘ └┘ └┘ └───────┘ ┴ ┴ ┴ ┴└────┘ ┴└┘ └┘
pid ───┘ └┘ └┘ └───────┘ ┴ ┴ ┴ └─────┘ └─┘ ┴┴
st ────────────────────────────────────────────┘└───────────────┘└────┘
354
355 /-- `of x` is the canonical injection from the type to the free group over that type by sending each
356 element to the equivalence class of the letter that is the element. -/
357 def of (x : α) : free_group α :=
id ┴ └────────┘ ┴
src └────────┘
typ ┴ └────────┘ ┴
doc └────────┘
358 mk [(x, tt)]
id └┘ ┴┴┴ └┘ ┴
src └┘ ┴┴ └┘ ┴
typ └┘ ┴┴┴ └┘ ┴
359
360 theorem red.exact : mk L₁ = mk L₂ ↔ join red L₁ L₂ :=
id └┘ └┘ ┴ └┘ └┘ ┴ └──┘ └─┘ └┘ └┘
src └┘ ┴ └┘ ┴ └──┘ └─┘
typ └┘ └┘ ┴ └┘ └┘ ┴ └──┘ └─┘ └┘ └┘
doc └─┘
361 calc (mk L₁ = mk L₂) ↔ eqv_gen red.step L₁ L₂ : iff.intro (quot.exact _) quot.eqv_gen_sound
id └┘ └┘ ┴ └┘ └┘ └─────┘ └──────┘ └┘ └┘ └───────┘ └────────┘ └────────────────┘
src └┘ ┴ └┘ └─────┘ └──────┘ └───────┘ └────────┘ └────────────────┘
typ └┘ └┘ ┴ └┘ └┘ └─────┘ └──────┘ └┘ └┘ └───────┘ └────────┘ └────────────────┘
doc └──────┘
362 ... ↔ join red L₁ L₂ : eqv_gen_step_iff_join_red
id └──┘ └─┘ └┘ └┘ └───────────────────────┘
src └──┘ └─┘ └───────────────────────┘
typ └──┘ └─┘ └┘ └┘ └───────────────────────┘
doc └─┘
363
364 /-- The canonical injection from the type to the free group is an injection. -/
365 theorem of.inj {x y : α} (H : of x = of y) : x = y :=
id ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └┘ ┴ └┘ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └┘ └┘
366 let ⟨L₁, hx, hy⟩ := red.exact.1 H in
id └─┘ └───────┘┴ ┴
src └───────┘┴
typ └─┘ └───────┘┴ ┴
367 by simp [red.singleton_iff] at hx hy; cc
id └───────────────┘
src └────┘└───────────────┘└────────┘ └──
typ └────┘└───────────────┘└────────┘ └──
doc └────┘└───────────────┘└────────┘ └──
txt └────┘ └────────┘ └──
par └────┘ └────────┘ └──
pid ┴┴ ┴┴└──────┘ └
st └──────────────────────────────────────
368
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
369 section to_group
370
371 variables {β : Type v} [group β] (f : α → β) {x y : free_group α}
id ┴ └───┘ └────────┘
src └───┘ └────────┘
typ ┴ └───┘ └────────┘
doc └────────┘
372
373 def to_group.aux : list (α × bool) → β :=
id └──┘ ┴ ┴ └──┘ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴ └──┘ ┴
374 λ L, list.prod $ L.map $ λ x, cond x.2 (f x.1) (f x.1)⁻¹
id ┴ └───────┘ ┴└──┘ ┴ └──┘ ┴┴ ┴ ┴┴ ┴ ┴┴ └┘
src └───────┘ └──┘ └──┘ ┴ ┴ ┴ └┘
typ ┴ └───────┘ ┴└──┘ ┴ └──┘ ┴┴ ┴ ┴┴ ┴ ┴┴ └┘
doc └───────┘
375
376 theorem red.step.to_group {f : α → β} (H : red.step L₁ L₂) :
id ┴ ┴ └──────┘ └┘ └┘
src └──────┘
typ ┴ ┴ └──────┘ └┘ └┘
doc └──────┘
377 to_group.aux f L₁ = to_group.aux f L₂ :=
id └──────────┘ ┴ └┘ ┴ └──────────┘ ┴ └┘
src └──────────┘ ┴ └──────────┘
typ └──────────┘ ┴ └┘ ┴ └──────────┘ ┴ └┘
378 by cases H with _ _ _ b; cases b; simp [to_group.aux]
id ┴ ┴ └──────────┘
src └────┘ └───────────┘ └────┘ └────┘└──────────┘└─
typ └────┘┴└───────────┘ └────┘┴ └────┘└──────────┘└─
doc └────┘ └───────────┘ └────┘ └────┘ └─
txt └────┘ └───────────┘ └────┘ └────┘ └─
par └────┘ └───────────┘ └────┘ └────┘ └─
pid ┴ └───────────┘ ┴ ┴┴ ┴└
st └───────────────────────────────────────────────────
379
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
380 /-- If `β` is a group, then any function from `α` to `β`
381 extends uniquely to a group homomorphism from
382 the free group over `α` to `β` -/
383 def to_group : free_group α → β :=
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
doc └────────┘
384 quot.lift (to_group.aux f) $ λ L₁ L₂ H, red.step.to_group H
id └───────┘ └──────────┘ ┴ └┘ └┘ ┴ └───────────────┘ ┴
src └──────────┘ └───────────────┘
typ └───────┘ └──────────┘ ┴ └┘ └┘ ┴ └───────────────┘ ┴
385
386 variable {f}
387
388 @[simp] lemma to_group.mk : to_group f (mk L) =
id └──────┘ ┴ └┘ ┴ ┴
src └──────┘ └┘ ┴
typ └──────┘ ┴ └┘ ┴ ┴
doc └──┘ └──────┘
389 list.prod (L.map $ λ x, cond x.2 (f x.1) (f x.1)⁻¹) :=
id └───────┘ ┴└──┘ ┴ └──┘ ┴┴ ┴ ┴┴ ┴ ┴┴ └┘
src └───────┘ └──┘ └──┘ ┴ ┴ ┴ └┘
typ └───────┘ ┴└──┘ ┴ └──┘ ┴┴ ┴ ┴┴ ┴ ┴┴ └┘
doc └───────┘
390 rfl
id └─┘
src └─┘
typ └─┘
391
392 @[simp] lemma to_group.of {x} : to_group f (of x) = f x :=
id └──────┘ ┴ └┘ ┴ ┴ ┴ ┴
src └──────┘ └┘ ┴
typ └──────┘ ┴ └┘ ┴ ┴ ┴ ┴
doc └──┘ └──────┘ └┘
393 one_mul _
id └─────┘
src └─────┘
typ └─────┘
394
395 instance to_group.is_group_hom : is_group_hom (to_group f) :=
id └──────────┘ └──────┘ ┴
src └──────────┘ └──────┘
typ └──────────┘ └──────┘ ┴
doc └──────────┘ └──────┘
396 { map_mul := by rintros ⟨L₁⟩ ⟨L₂⟩; simp }
src └───────────────┘ └───┘
typ └───────────────┘ └───┘
doc └───────────────┘ └───┘
txt └───────────────┘ └───┘
par └───────────────┘ └───┘
pid └────────┘ ┴
st └───────────────────────┘
397
398 @[simp] lemma to_group.mul : to_group f (x * y) = to_group f x * to_group f y :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src └──────┘ ┴ ┴ └──────┘ ┴ └──────┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └──┘ └──────┘ └──────┘ └──────┘
399 is_mul_hom.map_mul _ _ _
id └────────────────┘
src └────────────────┘
typ └────────────────┘
400
401 @[simp] lemma to_group.one : to_group f 1 = 1 :=
id └──────┘ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴
doc └──┘ └──────┘
402 is_group_hom.map_one _
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
403
404 @[simp] lemma to_group.inv : to_group f x⁻¹ = (to_group f x)⁻¹ :=
id └──────┘ ┴ ┴└┘ ┴ └──────┘ ┴ ┴ └┘
src └──────┘ └┘ ┴ └──────┘ └┘
typ └──────┘ ┴ ┴└┘ ┴ └──────┘ ┴ ┴ └┘
doc └──┘ └──────┘ └──────┘
405 is_group_hom.map_inv _ _
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
406
407 theorem to_group.unique (g : free_group α → β) [is_group_hom g]
id └────────┘ ┴ ┴ └──────────┘ ┴
src └────────┘ └──────────┘
typ └────────┘ ┴ ┴ └──────────┘ ┴
doc └────────┘ └──────────┘
408 (hg : ∀ x, g (of x) = f x) : ∀{x}, g x = to_group f x :=
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
src └┘ ┴ ┴ └──────┘
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └┘ └──────┘
409 by rintros ⟨L⟩; exact list.rec_on L (is_group_hom.map_one g)
id └─────────┘ ┴ └──────────────────┘
src └─────────┘ └────┘└─────────┘┴ ┴ └──────────────────┘┴ └┘
typ └─────────┘ └────┘└─────────┘┴┴┴ └──────────────────┘┴ └┘
doc └─────────┘ └────┘ ┴ ┴ └──────────────────┘┴ └┘
txt └─────────┘ └────┘ ┴ ┴ ┴ └┘
par └─────────┘ └────┘ ┴ ┴ ┴ └┘
pid └──┘ ┴ ┴ ┴ ┴ └┘
st └──────────────────────────────────────────────────────────
410 (λ ⟨x, b⟩ t (ih : g (mk t) = _), bool.rec_on b
id ┴ ┴ ┴ └─────────┘
src └┘ └┘ └────────┘ ┴ ┴ └┘┴└───┘└─────────┘┴ └
typ └┘┴└┘┴└────────┘ ┴ ┴ └┘┴└───┘└─────────┘┴ └
doc └┘ └┘ └────────┘ ┴ ┴ └┘ └───┘ ┴ └
txt └┘ └┘ └────────┘ ┴ ┴ └┘ └───┘ ┴ └
par └┘ └┘ └────────┘ ┴ ┴ └┘ └───┘ ┴ └
pid └┘ └┘ └────────┘ ┴ ┴ └┘ └───┘ ┴ └
st ───────────────────────────────────────────────
411 (show g ((of x)⁻¹ * mk t) = to_group f (mk ((x, ff) :: t)),
id └┘ ┴ ┴ ┴ └┘
src ─┘ ┴ ┴ ┴ ┴└┘┴┴┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘└┘└┘ ┴ └───
typ ─┘ ┴ ┴ ┴ ┴└┘┴┴┴ ┴ └┘┴┴ ┴ ┴ ┴ ┴ └┘└┘└┘ ┴ └───
doc ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └───
txt ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └───
par ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └───
pid ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └───
st ──────────────────────────────────────────────────────────────
412 by simp [is_mul_hom.map_mul g, is_group_hom.map_inv g, hg, ih, to_group, to_group.aux])
id └────────────────┘ ┴ └──────────────────┘ ┴ └┘ └┘ └──────┘ └──────────┘
src ───────┘└────┘└────────────────┘┴ └┘└──────────────────┘┴ └┘ └┘ └┘└──────┘└┘└──────────┘┴└─
typ ───────┘└────┘└────────────────┘┴┴└┘└──────────────────┘┴┴└┘└┘└┘└┘└┘└──────┘└┘└──────────┘┴└─
doc ───────┘└────┘ ┴ └┘└──────────────────┘┴ └┘ └┘ └┘└──────┘└┘ ┴└─
txt ───────┘└────┘ ┴ └┘ ┴ └┘ └┘ └┘ └┘ ┴└─
par ───────┘└────┘ ┴ └┘ ┴ └┘ └┘ └┘ └┘ ┴└─
pid ─────────────┘ ┴ └┘ ┴ └┘ └┘ └┘ └┘ └──
st ──────┘└──────────────────────────────────────────────────────────────────────────────────┘└─
413 (show g (of x * mk t) = to_group f (mk ((x, tt) :: t)),
id ┴ └┘ ┴ └──────┘ ┴ └┘ └┘
src ─┘ ┴ ┴ └┘┴ ┴ ┴ ┴ └┘ ┴└──────┘┴ ┴ └┘┴ └┘└┘└┘ ┴ └───
typ ─┘ ┴┴┴ └┘┴ ┴ ┴ ┴ └┘┴┴└──────┘┴┴┴ └┘┴ └┘└┘└┘ ┴ └───
doc ─┘ ┴ ┴ └┘┴ ┴ ┴ ┴ └┘ ┴└──────┘┴ ┴ ┴ └┘ └┘ ┴ └───
txt ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └───
par ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └───
pid ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ └───
st ──────────────────────────────────────────────────────────
414 by simp [is_mul_hom.map_mul g, is_group_hom.map_inv g, hg, ih, to_group, to_group.aux]))
id └────────────────┘ ┴ └──────────────────┘ ┴ └┘ └┘ └──────┘ └──────────┘
src ───────┘└────┘└────────────────┘┴ └┘└──────────────────┘┴ └┘ └┘ └┘└──────┘└┘└──────────┘┴└──
typ ───────┘└────┘└────────────────┘┴┴└┘└──────────────────┘┴┴└┘└┘└┘└┘└┘└──────┘└┘└──────────┘┴└──
doc ───────┘└────┘ ┴ └┘└──────────────────┘┴ └┘ └┘ └┘└──────┘└┘ ┴└──
txt ───────┘└────┘ ┴ └┘ ┴ └┘ └┘ └┘ └┘ ┴└──
par ───────┘└────┘ ┴ └┘ ┴ └┘ └┘ └┘ └┘ ┴└──
pid ─────────────┘ ┴ └┘ ┴ └┘ └┘ └┘ └┘ └─┘└
st ──────┘└──────────────────────────────────────────────────────────────────────────────────┘└──
415
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
416
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
417 theorem to_group.of_eq (x : free_group α) : to_group of x = x :=
id └────────┘ ┴ └──────┘ └┘ ┴ ┴ ┴
src └────────┘ └──────┘ └┘ ┴
typ └────────┘ ┴ └──────┘ └┘ ┴ ┴ ┴
doc └────────┘ └──────┘ └┘
418 eq.symm $ to_group.unique id (λ x, rfl)
id └─────┘ └─────────────┘ └┘ ┴ └─┘
src └─────┘ └─────────────┘ └┘ └─┘
typ └─────┘ └─────────────┘ └┘ ┴ └─┘
419
420 theorem to_group.range_subset {s : set β} [is_subgroup s] (H : set.range f ⊆ s) :
id └─┘ ┴ └─────────┘ ┴ └───────┘ ┴ ┴ ┴
src └─┘ └─────────┘ └───────┘ ┴
typ └─┘ ┴ └─────────┘ ┴ └───────┘ ┴ ┴ ┴
doc └─────────┘ └───────┘
421 set.range (to_group f) ⊆ s :=
id └───────┘ └──────┘ ┴ ┴ ┴
src └───────┘ └──────┘ ┴
typ └───────┘ └──────┘ ┴ ┴ ┴
doc └───────┘ └──────┘
422 by rintros _ ⟨⟨L⟩, rfl⟩; exact list.rec_on L (is_submonoid.one_mem s)
id └─────────┘ ┴ └──────────────────┘ ┴
src └──────────────────┘ └────┘└─────────┘┴ ┴ └──────────────────┘┴ └┘
typ └──────────────────┘ └────┘└─────────┘┴┴┴ └──────────────────┘┴┴└┘
doc └──────────────────┘ └────┘ ┴ ┴ ┴ └┘
txt └──────────────────┘ └────┘ ┴ ┴ ┴ └┘
par └──────────────────┘ └────┘ ┴ ┴ ┴ └┘
pid └───────────┘ ┴ ┴ ┴ ┴ └┘
st └───────────────────────────────────────────────────────────────────
423 (λ ⟨x, b⟩ tl ih, bool.rec_on b
id ┴ └─────────┘
src └┘ └┘ └───────┘└─────────┘┴ └
typ └┘ └┘┴└───────┘└─────────┘┴ └
doc └┘ └┘ └───────┘ ┴ └
txt └┘ └┘ └───────┘ ┴ └
par └┘ └┘ └───────┘ ┴ └
pid └┘ └┘ └───────┘ ┴ └
st ───────────────────────────────
424 (by simp at ih ⊢; from is_submonoid.mul_mem
id └──────────────────┘
src ───┘ ┴└──────────┘└┘└───┘└──────────────────┘└
typ ───┘ ┴└──────────┘└─────┘└──────────────────┘└
doc ───┘ ┴└──────────┘└┘└───┘ └
txt ───┘ ┴└──────────┘└┘└───┘ └
par ───┘ ┴└──────────┘└─────┘ └
pid ───┘ └──────────────────┘ └
st ──────┘└────────────────────────────────────────
425 (is_subgroup.inv_mem $ H ⟨x, rfl⟩) ih)
id └─────────────────┘ ┴ ┴ └─┘ └┘
src ─────┘ └─────────────────┘┴ ┴ ┴ └┘└─┘└─┘ └─
typ ─────┘ └─────────────────┘┴ ┴┴┴ ┴└┘└─┘└─┘└┘└─
doc ─────┘ ┴ ┴ ┴ └┘ └─┘ └─
txt ─────┘ ┴ ┴ ┴ └┘ └─┘ └─
par ─────┘ ┴ ┴ ┴ └┘ └─┘ └─
pid ─────┘ ┴ ┴ ┴ └┘ └─┘ └─
st ──────────────────────────────────────────┘└─
426 (by simp at ih ⊢; from is_submonoid.mul_mem (H ⟨x, rfl⟩) ih))
id └──────────────────┘ ┴ ┴ └─┘ └┘
src ───┘ ┴└──────────┘└┘└───┘└──────────────────┘┴ ┴ └┘└─┘└─┘ └──
typ ───┘ ┴└──────────┘└─────┘└──────────────────┘┴ ┴┴ ┴└┘└─┘└─┘└┘└──
doc ───┘ ┴└──────────┘└┘└───┘ ┴ ┴ └┘ └─┘ └──
txt ───┘ ┴└──────────┘└┘└───┘ ┴ ┴ └┘ └─┘ └──
par ───┘ ┴└──────────┘└─────┘ ┴ ┴ └┘ └─┘ └──
pid ───┘ └──────────────────┘ ┴ ┴ └┘ └─┘ └┘└
st ──────┘└──────────────────────────────────────────────────────┘└──
427
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
428 theorem to_group.range_eq_closure :
429 set.range (to_group f) = group.closure (set.range f) :=
id └───────┘ └──────┘ ┴ ┴ └───────────┘ └───────┘ ┴
src └───────┘ └──────┘ ┴ └───────────┘ └───────┘
typ └───────┘ └──────┘ ┴ ┴ └───────────┘ └───────┘ ┴
doc └───────┘ └──────┘ └───────────┘ └───────┘
430 set.subset.antisymm
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
431 (to_group.range_subset group.subset_closure)
id └───────────────────┘ └──────────────────┘
src └───────────────────┘ └──────────────────┘
typ └───────────────────┘ └──────────────────┘
432 (group.closure_subset $ λ y ⟨x, hx⟩, ⟨of x, by simpa⟩)
id └──────────────────┘ ┴ ┴┴ └┘
src └──────────────────┘ └┘ └───┘
typ └──────────────────┘ ┴ ┴┴ └┘ └───┘
doc └┘ └───┘
txt └───┘
par └───┘
st └────┘
433
434 end to_group
435
436 section map
437
438 variables {β : Type v} (f : α → β) {x y : free_group α}
id └────────┘
src └────────┘
typ └────────┘
doc └────────┘
439
440 def map.aux (L : list (α × bool)) : list (β × bool) :=
id └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘
src └──┘ ┴ └──┘ └──┘ ┴ └──┘
typ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘
441 L.map $ λ x, (f x.1, x.2)
id ┴└──┘ ┴ ┴┴ ┴┴ ┴┴
src └──┘ ┴ ┴ ┴
typ ┴└──┘ ┴ ┴┴ ┴┴ ┴┴
442
443 /-- Any function from `α` to `β` extends uniquely
444 to a group homomorphism from the free group
445 ver `α` to the free group over `β`. -/
446 def map (x : free_group α) : free_group β :=
id └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘
447 x.lift_on (λ L, mk $ map.aux f L) $
id ┴└──────┘ ┴ └┘ └─────┘ ┴ ┴
src └──────┘ └┘ └─────┘
typ ┴└──────┘ ┴ └┘ └─────┘ ┴ ┴
448 λ L₁ L₂ H, quot.sound $ by cases H; simp [map.aux]
id └┘ └┘ ┴ └────────┘ ┴ └─────┘
src └────────┘ └────┘ └────┘└─────┘└─
typ └┘ └┘ ┴ └────────┘ └────┘┴ └────┘└─────┘└─
doc └────┘ └────┘ └─
txt └────┘ └────┘ └─
par └────┘ └────┘ └─
pid ┴ ┴┴ ┴└
st └────────────────────────
449
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
450 instance map.is_group_hom : is_group_hom (map f) :=
id └──────────┘ └─┘ ┴
src └──────────┘ └─┘
typ └──────────┘ └─┘ ┴
doc └──────────┘ └─┘
451 { map_mul := by rintros ⟨L₁⟩ ⟨L₂⟩; simp [map, map.aux] }
id └─┘ └─────┘
src └───────────────┘ └────┘└─┘└┘└─────┘└┘
typ └───────────────┘ └────┘└─┘└┘└─────┘└┘
doc └───────────────┘ └────┘└─┘└┘ └┘
txt └───────────────┘ └────┘ └┘ └┘
par └───────────────┘ └────┘ └┘ └┘
pid └────────┘ ┴┴ └┘ ┴┴
st └──────────────────────────────────────┘
452
453 variable {f}
454
455 @[simp] lemma map.mk : map f (mk L) = mk (L.map (λ x, (f x.1, x.2))) :=
id └─┘ ┴ └┘ ┴ ┴ └┘ ┴└──┘ ┴ ┴┴ ┴┴ ┴┴
src └─┘ └┘ ┴ └┘ └──┘ ┴ ┴ ┴
typ └─┘ ┴ └┘ ┴ ┴ └┘ ┴└──┘ ┴ ┴┴ ┴┴ ┴┴
doc └──┘ └─┘
456 rfl
id └─┘
src └─┘
typ └─┘
457
458 @[simp] lemma map.id : map id x = x :=
id └─┘ └┘ ┴ ┴ ┴
src └─┘ └┘ ┴
typ └─┘ └┘ ┴ ┴ ┴
doc └──┘ └─┘
459 have H1 : (λ (x : α × bool), x) = id := rfl,
id ┴ ┴ └──┘ ┴ ┴ └┘ └─┘
src ┴ └──┘ ┴ └┘ └─┘
typ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘
460 by rcases x with ⟨L⟩; simp [H1]
id ┴ └┘
src └─────┘ └───────┘ └────┘ └─
typ └─────┘┴└───────┘ └────┘└┘└─
doc └─────┘ └───────┘ └────┘ └─
txt └─────┘ └───────┘ └────┘ └─
par └─────┘ └───────┘ └────┘ └─
pid ┴ └───────┘ ┴┴ ┴└
st └─────────────────────────────
461
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
462 @[simp] lemma map.id' : map (λ z, z) x = x := map.id
id └─┘ ┴ ┴ ┴ ┴ ┴ └────┘
src └─┘ ┴ └────┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ └────┘
doc └──┘ └─┘
463
464 theorem map.comp {γ : Type w} {f : α → β} {g : β → γ} {x} :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
465 map g (map f x) = map (g ∘ f) x :=
id └─┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴ └─┘ ┴
typ └─┘ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
doc └─┘ └─┘ └─┘
466 by rcases x with ⟨L⟩; simp
id ┴
src └─────┘ └───────┘ └────
typ └─────┘┴└───────┘ └────
doc └─────┘ └───────┘ └────
txt └─────┘ └───────┘ └────
par └─────┘ └───────┘ └────
pid ┴ └───────┘ └
st └────────────────────────
467
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
468 @[simp] lemma map.of {x} : map f (of x) = of (f x) := rfl
id └─┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─┘
src └─┘ └┘ ┴ └┘ └─┘
typ └─┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─┘
doc └──┘ └─┘ └┘ └┘
469
470 @[simp] lemma map.mul : map f (x * y) = map f x * map f y :=
id └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
doc └──┘ └─┘ └─┘ └─┘
471 is_mul_hom.map_mul _ x y
id └────────────────┘ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴
472
473 @[simp] lemma map.one : map f 1 = 1 :=
id └─┘ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴
doc └──┘ └─┘
474 is_group_hom.map_one _
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
475
476 @[simp] lemma map.inv : map f x⁻¹ = (map f x)⁻¹ :=
id └─┘ ┴ ┴└┘ ┴ └─┘ ┴ ┴ └┘
src └─┘ └┘ ┴ └─┘ └┘
typ └─┘ ┴ ┴└┘ ┴ └─┘ ┴ ┴ └┘
doc └──┘ └─┘ └─┘
477 is_group_hom.map_inv _ x
id └──────────────────┘ ┴
src └──────────────────┘
typ └──────────────────┘ ┴
doc └──────────────────┘
478
479 theorem map.unique (g : free_group α → free_group β) [is_group_hom g]
id └────────┘ ┴ └────────┘ ┴ └──────────┘ ┴
src └────────┘ └────────┘ └──────────┘
typ └────────┘ ┴ └────────┘ ┴ └──────────┘ ┴
doc └────────┘ └────────┘ └──────────┘
480 (hg : ∀ x, g (of x) = of (f x)) : ∀{x}, g x = map f x :=
id ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src └┘ ┴ └┘ ┴ └─┘
typ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
doc └┘ └┘ └─┘
481 by rintros ⟨L⟩; exact list.rec_on L (is_group_hom.map_one g)
id └─────────┘ ┴ └──────────────────┘
src └─────────┘ └────┘└─────────┘┴ ┴ └──────────────────┘┴ └┘
typ └─────────┘ └────┘└─────────┘┴┴┴ └──────────────────┘┴ └┘
doc └─────────┘ └────┘ ┴ ┴ └──────────────────┘┴ └┘
txt └─────────┘ └────┘ ┴ ┴ ┴ └┘
par └─────────┘ └────┘ ┴ ┴ ┴ └┘
pid └──┘ ┴ ┴ ┴ ┴ └┘
st └──────────────────────────────────────────────────────────
482 (λ ⟨x, b⟩ t (ih : g (mk t) = map f (mk t)), bool.rec_on b
id ┴ ┴ ┴ └─────────┘
src └┘ └┘ └────────┘ ┴ ┴ └┘┴┴ ┴ ┴ ┴ └──┘└─────────┘┴ └
typ └┘┴└┘┴└────────┘ ┴ ┴ └┘┴┴ ┴ ┴ ┴ └──┘└─────────┘┴ └
doc └┘ └┘ └────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └
txt └┘ └┘ └────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └
par └┘ └┘ └────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └
pid └┘ └┘ └────────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └
st ──────────────────────────────────────────────────────────
483 (show g ((of x)⁻¹ * mk t) = map f ((of x)⁻¹ * mk t),
id └┘ ┴ ┴
src ─┘ ┴ ┴ ┴ ┴└┘┴┴┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
typ ─┘ ┴ ┴ ┴ ┴└┘┴┴┴ ┴ └┘┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
doc ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
txt ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
par ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
pid ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ───────────────────────────────────────────────────────
484 by simp [is_mul_hom.map_mul g, is_group_hom.map_inv g, hg, ih])
id └────────────────┘ ┴ └──────────────────┘ ┴ └┘ └┘
src ───────┘└────┘└────────────────┘┴ └┘└──────────────────┘┴ └┘ └┘ ┴└─
typ ───────┘└────┘└────────────────┘┴┴└┘└──────────────────┘┴┴└┘└┘└┘└┘┴└─
doc ───────┘└────┘ ┴ └┘└──────────────────┘┴ └┘ └┘ ┴└─
txt ───────┘└────┘ ┴ └┘ ┴ └┘ └┘ ┴└─
par ───────┘└────┘ ┴ └┘ ┴ └┘ └┘ ┴└─
pid ─────────────┘ ┴ └┘ ┴ └┘ └┘ └──
st ──────┘└──────────────────────────────────────────────────────────┘└─
485 (show g (of x * mk t) = map f (of x * mk t),
id ┴ ┴ └─┘ ┴ └┘ └┘
src ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴└─┘┴ ┴ └┘┴ ┴ ┴└┘┴ └──
typ ─┘ ┴┴┴ ┴ ┴ ┴ ┴ └┘┴┴└─┘┴┴┴ └┘┴ ┴ ┴└┘┴ └──
doc ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴└─┘┴ ┴ └┘┴ ┴ ┴ ┴ └──
txt ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
par ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
pid ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ───────────────────────────────────────────────
486 by simp [is_mul_hom.map_mul g, hg, ih]))
id └────────────────┘ ┴ └┘ └┘
src ───────┘└────┘└────────────────┘┴ └┘ └┘ ┴└──
typ ───────┘└────┘└────────────────┘┴┴└┘└┘└┘└┘┴└──
doc ───────┘└────┘ ┴ └┘ └┘ ┴└──
txt ───────┘└────┘ ┴ └┘ └┘ ┴└──
par ───────┘└────┘ ┴ └┘ └┘ ┴└──
pid ─────────────┘ ┴ └┘ └┘ └─┘└
st ──────┘└──────────────────────────────────┘└──
487
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
488 /-- Equivalent types give rise to equivalent free groups. -/
489 def free_group_congr {α β} (e : α ≃ β) : free_group α ≃ free_group β :=
id ┴ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴
src ┴ └────────┘ ┴ └────────┘
typ ┴ ┴ ┴ └────────┘ ┴ ┴ └────────┘ ┴
doc ┴ └────────┘ ┴ └────────┘
490 ⟨map e, map e.symm,
id └─┘ ┴ └─┘ ┴└───┘
src └─┘ └─┘ └───┘
typ └─┘ ┴ └─┘ ┴└───┘
doc └─┘ └─┘
491 λ x, by simp [function.comp, map.comp],
id ┴ └───────────┘ └──────┘
src └────┘└───────────┘└┘└──────┘┴
typ ┴ └────┘└───────────┘└┘└──────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └─────────────────────────────┘
492 λ x, by simp [function.comp, map.comp]⟩
id ┴ └───────────┘ └──────┘
src └────┘└───────────┘└┘└──────┘┴
typ ┴ └────┘└───────────┘└┘└──────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └─────────────────────────────┘
493
494 theorem map_eq_to_group : map f x = to_group (of ∘ f) x :=
id └─┘ ┴ ┴ ┴ └──────┘ └┘ ┴ ┴ ┴
src └─┘ ┴ └──────┘ └┘ ┴
typ └─┘ ┴ ┴ ┴ └──────┘ └┘ ┴ ┴ ┴
doc └─┘ └──────┘ └┘
495 eq.symm $ map.unique _ $ λ x, by simp
id └─────┘ └────────┘ ┴
src └─────┘ └────────┘ └────
typ └─────┘ └────────┘ ┴ └────
doc └────
txt └────
par └────
pid └
st └─────
496
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
497 end map
498
499 section prod
500
501 variables [group α] (x y : free_group α)
id └───┘ └────────┘
src └───┘ └────────┘
typ └───┘ └────────┘
doc └────────┘
502
503 /-- If `α` is a group, then any function from `α` to `α`
504 extends uniquely to a homomorphism from the
505 free group over `α` to `α`. This is the multiplicative
506 version of `sum`. -/
507 def prod : α :=
id ┴
typ ┴
508 to_group id x
id └──────┘ └┘ ┴
src └──────┘ └┘
typ └──────┘ └┘ ┴
doc └──────┘
509
510 variables {x y}
511
512 @[simp] lemma prod_mk :
doc └──┘
513 prod (mk L) = list.prod (L.map $ λ x, cond x.2 x.1 x.1⁻¹) :=
id └──┘ └┘ ┴ ┴ └───────┘ ┴└──┘ ┴ └──┘ ┴┴ ┴┴ ┴┴ └┘
src └──┘ └┘ ┴ └───────┘ └──┘ └──┘ ┴ ┴ ┴ └┘
typ └──┘ └┘ ┴ ┴ └───────┘ ┴└──┘ ┴ └──┘ ┴┴ ┴┴ ┴┴ └┘
doc └──┘ └───────┘
514 rfl
id └─┘
src └─┘
typ └─┘
515
516 @[simp] lemma prod.of {x : α} : prod (of x) = x :=
id ┴ └──┘ └┘ ┴ ┴ ┴
src └──┘ └┘ ┴
typ ┴ └──┘ └┘ ┴ ┴ ┴
doc └──┘ └──┘ └┘
517 to_group.of
id └─────────┘
src └─────────┘
typ └─────────┘
518
519 instance prod.is_group_hom : is_group_hom (@prod α _) :=
id └──────────┘ └──┘ ┴
src └──────────┘ └──┘
typ └──────────┘ └──┘ ┴
doc └──────────┘ └──┘
520 to_group.is_group_hom
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
521
522 @[simp] lemma prod.mul : prod (x * y) = prod x * prod y :=
id └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
src └──┘ ┴ ┴ └──┘ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴
doc └──┘ └──┘ └──┘ └──┘
523 to_group.mul
id └──────────┘
src └──────────┘
typ └──────────┘
524
525 @[simp] lemma prod.one : prod (1:free_group α) = 1 :=
id └──┘ └────────┘ ┴ ┴
src └──┘ └────────┘ ┴
typ └──┘ └────────┘ ┴ ┴
doc └──┘ └──┘ └────────┘
526 to_group.one
id └──────────┘
src └──────────┘
typ └──────────┘
527
528 @[simp] lemma prod.inv : prod x⁻¹ = (prod x)⁻¹ :=
id └──┘ ┴└┘ ┴ └──┘ ┴ └┘
src └──┘ └┘ ┴ └──┘ └┘
typ └──┘ ┴└┘ ┴ └──┘ ┴ └┘
doc └──┘ └──┘ └──┘
529 to_group.inv
id └──────────┘
src └──────────┘
typ └──────────┘
530
531 lemma prod.unique (g : free_group α → α) [is_group_hom g]
id └────────┘ ┴ ┴ └──────────┘ ┴
src └────────┘ └──────────┘
typ └────────┘ ┴ ┴ └──────────┘ ┴
doc └────────┘ └──────────┘
532 (hg : ∀ x, g (of x) = x) {x} :
id ┴ ┴ └┘ ┴ ┴ ┴
src └┘ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴
doc └┘
533 g x = prod x :=
id ┴ ┴ ┴ └──┘ ┴
src ┴ └──┘
typ ┴ ┴ ┴ └──┘ ┴
doc └──┘
534 to_group.unique g hg
id └─────────────┘ ┴ └┘
src └─────────────┘
typ └─────────────┘ ┴ └┘
535
536 end prod
537
538 theorem to_group_eq_prod_map {β : Type v} [group β] {f : α → β} {x} :
id └───┘ ┴ ┴ ┴
src └───┘
typ └───┘ ┴ ┴ ┴
539 to_group f x = prod (map f x) :=
id └──────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴
src └──────┘ ┴ └──┘ └─┘
typ └──────┘ ┴ ┴ ┴ └──┘ └─┘ ┴ ┴
doc └──────┘ └──┘ └─┘
540 eq.symm $ to_group.unique (prod ∘ map f) $ λ _, by simp
id └─────┘ └─────────────┘ └──┘ ┴ └─┘ ┴ ┴
src └─────┘ └─────────────┘ └──┘ ┴ └─┘ └────
typ └─────┘ └─────────────┘ └──┘ ┴ └─┘ ┴ ┴ └────
doc └──┘ └─┘ └────
txt └────
par └────
pid └
st └─────
541
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
542 section sum
543
544 variables [add_group α] (x y : free_group α)
id └───────┘ └────────┘
src └───────┘ └────────┘
typ └───────┘ └────────┘
doc └────────┘
545
546 /-- If `α` is a group, then any function from `α` to `α`
547 extends uniquely to a homomorphism from the
548 free group over `α` to `α`. This is the additive
549 version of `prod`. -/
550 def sum : α :=
id ┴
typ ┴
551 @prod (multiplicative _) _ x
id └──┘ └────────────┘ ┴
src └──┘ └────────────┘
typ └──┘ └────────────┘ ┴
doc └──┘
552
553 variables {x y}
554
555 @[simp] lemma sum_mk :
doc └──┘
556 sum (mk L) = list.sum (L.map $ λ x, cond x.2 x.1 (-x.1)) :=
id └─┘ └┘ ┴ ┴ └──────┘ ┴└──┘ ┴ └──┘ ┴┴ ┴┴ ┴┴┴
src └─┘ └┘ ┴ └──────┘ └──┘ └──┘ ┴ ┴ ┴ ┴
typ └─┘ └┘ ┴ ┴ └──────┘ ┴└──┘ ┴ └──┘ ┴┴ ┴┴ ┴┴┴
doc └─┘ └──────┘
557 rfl
id └─┘
src └─┘
typ └─┘
558
559 @[simp] lemma sum.of {x : α} : sum (of x) = x :=
id ┴ └─┘ └┘ ┴ ┴ ┴
src └─┘ └┘ ┴
typ ┴ └─┘ └┘ ┴ ┴ ┴
doc └──┘ └─┘ └┘
560 prod.of
id └─────┘
src └─────┘
typ └─────┘
561
562 instance sum.is_group_hom : is_group_hom (@sum α _) :=
id └──────────┘ └─┘ ┴
src └──────────┘ └─┘
typ └──────────┘ └─┘ ┴
doc └──────────┘ └─┘
563 prod.is_group_hom
id └───────────────┘
src └───────────────┘
typ └───────────────┘
564
565 @[simp] lemma sum.mul : sum (x * y) = sum x + sum y :=
id └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ ┴ ┴ └─┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴
doc └──┘ └─┘ └─┘ └─┘
566 prod.mul
id └──────┘
src └──────┘
typ └──────┘
567
568 @[simp] lemma sum.one : sum (1:free_group α) = 0 :=
id └─┘ └────────┘ ┴ ┴
src └─┘ └────────┘ ┴
typ └─┘ └────────┘ ┴ ┴
doc └──┘ └─┘ └────────┘
569 prod.one
id └──────┘
src └──────┘
typ └──────┘
570
571 @[simp] lemma sum.inv : sum x⁻¹ = -sum x :=
id └─┘ ┴└┘ ┴ ┴└─┘ ┴
src └─┘ └┘ ┴ ┴└─┘
typ └─┘ ┴└┘ ┴ ┴└─┘ ┴
doc └──┘ └─┘ └─┘
572 prod.inv
id └──────┘
src └──────┘
typ └──────┘
573
574 end sum
575
576 def free_group_empty_equiv_unit : free_group empty ≃ unit :=
id └────────┘ └───┘ ┴ └──┘
src └────────┘ └───┘ ┴ └──┘
typ └────────┘ └───┘ ┴ └──┘
doc └────────┘ ┴ └──┘
577 { to_fun := λ _, (),
id ┴ └┘
src └┘
typ ┴ └┘
578 inv_fun := λ _, 1,
id ┴
typ ┴
579 left_inv := by rintros ⟨_ | ⟨⟨⟨⟩, _⟩, _⟩⟩; refl,
src └────────────────────────┘ └──┘
typ └────────────────────────┘ └──┘
doc └────────────────────────┘ └──┘
txt └────────────────────────┘ └──┘
par └────────────────────────┘ └──┘
pid └─────────────────┘
st └───────────────────────────────┘
580 right_inv := λ ⟨⟩, rfl }
id ┴ └─┘
src ┴ └─┘
typ ┴ └─┘
581
582 def free_group_unit_equiv_int : free_group unit ≃ int :=
id └────────┘ └──┘ ┴ └─┘
src └────────┘ └──┘ ┴ └─┘
typ └────────┘ └──┘ ┴ └─┘
doc └────────┘ └──┘ ┴
583 { to_fun := λ x, sum $ map (λ _, 1) x,
id ┴ └─┘ └─┘ ┴ ┴
src └─┘ └─┘
typ ┴ └─┘ └─┘ ┴ ┴
doc └─┘ └─┘
584 inv_fun := λ x, of () ^ x,
id ┴ └┘ └┘ ┴ ┴
src └┘ └┘ ┴
typ ┴ └┘ └┘ ┴ ┴
doc └┘
585 left_inv := by rintros ⟨L⟩; exact list.rec_on L rfl
id └─────────┘ ┴ └─┘
src └─────────┘ └────┘└─────────┘┴ ┴└─┘└
typ └─────────┘ └────┘└─────────┘┴┴┴└─┘└
doc └─────────┘ └────┘ ┴ ┴ └
txt └─────────┘ └────┘ ┴ ┴ └
par └─────────┘ └────┘ ┴ ┴ └
pid └──┘ ┴ ┴ ┴ └
st └─────────────────────────────────────
586 (λ ⟨⟨⟩, b⟩ tl ih, by cases b; simp [gpow_add] at ih ⊢; rw ih; refl),
id ┴ ┴ └──────┘ └┘
src ───┘ └┘┴└─┘ └───────┘ ┴└────┘ └┘└────┘└──────┘└───────┘└┘└─┘ └┘└──┘┴
typ ───┘ └┘┴└─┘ └───────┘ ┴└────┘┴└┘└────┘└──────┘└───────┘└┘└─┘└┘└┘└──┘┴
doc ───┘ └┘ └─┘ └───────┘ ┴└────┘ └┘└────┘ └───────┘└┘└─┘ └┘└──┘┴
txt ───┘ └┘ └─┘ └───────┘ ┴└────┘ └┘└────┘ └───────┘└┘└─┘ └┘└──┘┴
par ───┘ └┘ └─┘ └───────┘ ┴└────┘ └┘└────┘ └───────┘└┘└─┘ └┘└──┘┴
pid ───┘ └┘ └─┘ └───────┘ └─────┘ └──────┘ └────────────┘ └─────┘
st ───────────────────────┘└────────────────────────────────────┘└┘└────┘┴
587 right_inv := λ x, int.induction_on x (by simp)
id ┴ └──────────────┘ ┴
src └──────────────┘ └──┘
typ ┴ └──────────────┘ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
588 (λ i ih, by simp at ih; simp [gpow_add, ih])
id ┴ └┘ └──────┘ └┘
src └────────┘ └────┘└──────┘└┘ ┴
typ ┴ └┘ └────────┘ └────┘└──────┘└┘└┘┴
doc └────────┘ └────┘ └┘ ┴
txt └────────┘ └────┘ └┘ ┴
par └────────┘ └────┘ └┘ ┴
pid ┴└───┘ ┴┴ └┘ ┴
st └──────────────────────────────┘
589 (λ i ih, by simp at ih; simp [gpow_add, ih]) }
id ┴ └┘ └──────┘ └┘
src └────────┘ └────┘└──────┘└┘ ┴
typ ┴ └┘ └────────┘ └────┘└──────┘└┘└┘┴
doc └────────┘ └────┘ └┘ ┴
txt └────────┘ └────┘ └┘ ┴
par └────────┘ └────┘ └┘ ┴
pid ┴└───┘ ┴┴ └┘ ┴
st └──────────────────────────────┘
590
591 section category
592
593 variables {β : Type u}
594
595 instance : monad free_group.{u} :=
id └───┘ └────────┘
src └───┘ └────────┘
typ └───┘ └────────┘
doc └────────┘
596 { pure := λ α, of,
id ┴ └┘
src └┘
typ ┴ └┘
doc └┘
597 map := λ α β, map,
id ┴ ┴ └─┘
src └─┘
typ ┴ ┴ └─┘
doc └─┘
598 bind := λ α β x f, to_group f x }
id ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
src └──────┘
typ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘
599
600 @[elab_as_eliminator]
doc └────────────────┘
601 protected theorem induction_on
602 {C : free_group α → Prop}
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
603 (z : free_group α)
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
604 (C1 : C 1)
id ┴
typ ┴
605 (Cp : ∀ x, C $ pure x)
id ┴ ┴ └──┘ ┴
src └──┘
typ ┴ ┴ └──┘ ┴
606 (Ci : ∀ x, C (pure x) → C (pure x)⁻¹)
id ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ └┘
src └──┘ └──┘ └┘
typ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ └┘
607 (Cm : ∀ x y, C x → C y → C (x * y)) : C z :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
608 quot.induction_on z $ λ L, list.rec_on L C1 $ λ ⟨x, b⟩ tl ih,
id └───────────────┘ ┴ ┴ └─────────┘ ┴ └┘ ┴┴ ┴ └┘ └┘
src └───────────────┘ └─────────┘
typ └───────────────┘ ┴ ┴ └─────────┘ ┴ └┘ ┴┴ ┴ └┘ └┘
609 bool.rec_on b (Cm _ _ (Ci _ $ Cp x) ih) (Cm _ _ (Cp x) ih)
id └─────────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
src └─────────┘
typ └─────────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
610
611 @[simp] lemma map_pure (f : α → β) (x : α) : f <$> (pure x : free_group α) = pure (f x) :=
id ┴ ┴ ┴ ┴ └─┘ └──┘ ┴ └────────┘ ┴ ┴ └──┘ ┴ ┴
src └─┘ └──┘ └────────┘ ┴ └──┘
typ ┴ ┴ ┴ ┴ └─┘ └──┘ ┴ └────────┘ ┴ ┴ └──┘ ┴ ┴
doc └──┘ └────────┘
612 map.of
id └────┘
src └────┘
typ └────┘
613
614 @[simp] lemma map_one (f : α → β) : f <$> (1 : free_group α) = 1 :=
id ┴ ┴ ┴ └─┘ └────────┘ ┴ ┴
src └─┘ └────────┘ ┴
typ ┴ ┴ ┴ └─┘ └────────┘ ┴ ┴
doc └──┘ └────────┘
615 map.one
id └─────┘
src └─────┘
typ └─────┘
616
617 @[simp] lemma map_mul (f : α → β) (x y : free_group α) : f <$> (x * y) = f <$> x * f <$> y :=
id ┴ ┴ └────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴
src └────────┘ └─┘ ┴ ┴ └─┘ ┴ └─┘
typ ┴ ┴ └────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴
doc └──┘ └────────┘
618 map.mul
id └─────┘
src └─────┘
typ └─────┘
619
620 @[simp] lemma map_inv (f : α → β) (x : free_group α) : f <$> (x⁻¹) = (f <$> x)⁻¹ :=
id ┴ ┴ └────────┘ ┴ ┴ └─┘ ┴└┘ ┴ ┴ └─┘ ┴ └┘
src └────────┘ └─┘ └┘ ┴ └─┘ └┘
typ ┴ ┴ └────────┘ ┴ ┴ └─┘ ┴└┘ ┴ ┴ └─┘ ┴ └┘
doc └──┘ └────────┘
621 map.inv
id └─────┘
src └─────┘
typ └─────┘
622
623 @[simp] lemma pure_bind (f : α → free_group β) (x) : pure x >>= f = f x :=
id ┴ └────────┘ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴
src └────────┘ └──┘ └─┘ ┴
typ ┴ └────────┘ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴
doc └──┘ └────────┘
624 to_group.of
id └─────────┘
src └─────────┘
typ └─────────┘
625
626 @[simp] lemma one_bind (f : α → free_group β) : 1 >>= f = 1 :=
id ┴ └────────┘ ┴ └─┘ ┴ ┴
src └────────┘ └─┘ ┴
typ ┴ └────────┘ ┴ └─┘ ┴ ┴
doc └──┘ └────────┘
627 @@to_group.one _ f
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
628
629 @[simp] lemma mul_bind (f : α → free_group β) (x y : free_group α) : x * y >>= f = (x >>= f) * (y >>= f) :=
id ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴
src └────────┘ └────────┘ ┴ └─┘ ┴ └─┘ ┴ └─┘
typ ┴ └────────┘ ┴ └────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴
doc └──┘ └────────┘ └────────┘
630 to_group.mul
id └──────────┘
src └──────────┘
typ └──────────┘
631
632 @[simp] lemma inv_bind (f : α → free_group β) (x : free_group α) : x⁻¹ >>= f = (x >>= f)⁻¹ :=
id ┴ └────────┘ ┴ └────────┘ ┴ ┴└┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └┘
src └────────┘ └────────┘ └┘ └─┘ ┴ └─┘ └┘
typ ┴ └────────┘ ┴ └────────┘ ┴ ┴└┘ └─┘ ┴ ┴ ┴ └─┘ ┴ └┘
doc └──┘ └────────┘ └────────┘
633 to_group.inv
id └──────────┘
src └──────────┘
typ └──────────┘
634
635 instance : is_lawful_monad free_group.{u} :=
id └─────────────┘ └────────┘
src └─────────────┘ └────────┘
typ └─────────────┘ └────────┘
doc └────────┘
636 { id_map := λ α x, free_group.induction_on x (map_one id) (λ x, map_pure id x)
id ┴ ┴ ┴ └─────────────────────┘ ┴ └─────┘ └┘ ┴ └──────┘ └┘ ┴
src ┴ └─────────────────────┘ └─────┘ └┘ └──────┘ └┘
typ ┴ ┴ ┴ └─────────────────────┘ ┴ └─────┘ └┘ ┴ └──────┘ └┘ ┴
637 (λ x ih, by rw [map_inv, ih]) (λ x y ihx ihy, by rw [map_mul, ihx, ihy]),
id ┴ └┘ └─────┘ └┘ ┴ ┴ └─┘ └─┘ └─────┘ └─┘ └─┘
src └──┘└─────┘└┘ ┴ └──┘└─────┘└┘ └┘ ┴
typ ┴ └┘ └──┘└─────┘└┘└┘┴ ┴ ┴ └─┘ └─┘ └──┘└─────┘└┘└─┘└┘└─┘┴
doc └──┘ └┘ ┴ └──┘ └┘ └┘ ┴
txt └──┘ └┘ ┴ └──┘ └┘ └┘ ┴
par └──┘ └┘ ┴ └──┘ └┘ └┘ ┴
pid └┘ └┘ ┴ └┘ └┘ └┘ ┴
st └──────────┘└──┘┴ └──────────┘└───┘└───┘┴
638 pure_bind := λ α β x f, pure_bind f x,
id ┴ ┴ ┴ ┴ └───────┘ ┴ ┴
src └───────┘
typ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴
639 bind_assoc := λ α β γ x f g, free_group.induction_on x
id ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘ ┴
src └─────────────────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────────┘ ┴
640 (by iterate 3 { rw one_bind }) (λ x, by iterate 2 { rw pure_bind })
id └──────┘ ┴ └───────┘
src └──────────┘└─┘└──────┘┴┴ └──────────┘└─┘└───────┘┴┴
typ └──────────┘└─┘└──────┘┴┴ ┴ └──────────┘└─┘└───────┘┴┴
doc └──────────┘└─┘ ┴┴ └──────────┘└─┘ ┴┴
txt └──────────┘└─┘ ┴┴ └──────────┘└─┘ ┴┴
par └──────────┘└─┘ ┴┴ └──────────┘└─┘ ┴┴
pid ┴└─────┘ └┘ ┴└─────┘ └┘
st └───────────────────────┘└┘ └────────────────────────┘└┘
641 (λ x ih, by iterate 3 { rw inv_bind }; rw ih)
id ┴ └┘ └──────┘ └┘
src └──────────┘└─┘└──────┘┴┴ └─┘
typ ┴ └┘ └──────────┘└─┘└──────┘┴┴ └─┘└┘
doc └──────────┘└─┘ ┴┴ └─┘
txt └──────────┘└─┘ ┴┴ └─┘
par └──────────┘└─┘ ┴┴ └─┘
pid ┴└─────┘ └┘ ┴
st └───────────────────────┘└┘└──┘└┘
642 (λ x y ihx ihy, by iterate 3 { rw mul_bind }; rw [ihx, ihy]),
id ┴ ┴ └─┘ └─┘ └──────┘ └─┘ └─┘
src └──────────┘└─┘└──────┘┴┴ └──┘ └┘ ┴
typ ┴ ┴ └─┘ └─┘ └──────────┘└─┘└──────┘┴┴ └──┘└─┘└┘└─┘┴
doc └──────────┘└─┘ ┴┴ └──┘ └┘ ┴
txt └──────────┘└─┘ ┴┴ └──┘ └┘ ┴
par └──────────┘└─┘ ┴┴ └──┘ └┘ ┴
pid ┴└─────┘ └┘ └┘ └┘ ┴
st └───────────────────────┘└┘└───┘└─┘└───┘┴
643 bind_pure_comp_eq_map := λ α β f x, free_group.induction_on x
id ┴ ┴ ┴ ┴ └─────────────────────┘ ┴
src └─────────────────────┘
typ ┴ ┴ ┴ ┴ └─────────────────────┘ ┴
644 (by rw [one_bind, map_one]) (λ x, by rw [pure_bind, map_pure])
id └──────┘ └─────┘ ┴ └───────┘ └──────┘
src └──┘└──────┘└┘└─────┘┴ └──┘└───────┘└┘└──────┘┴
typ └──┘└──────┘└┘└─────┘┴ ┴ └──┘└───────┘└┘└──────┘┴
doc └──┘ └┘ ┴ └──┘ └┘ ┴
txt └──┘ └┘ ┴ └──┘ └┘ ┴
par └──┘ └┘ ┴ └──┘ └┘ ┴
pid └┘ └┘ ┴ └┘ └┘ ┴
st └───────────┘└───────┘┴ └────────────┘└────────┘┴
645 (λ x ih, by rw [inv_bind, map_inv, ih]) (λ x y ihx ihy, by rw [mul_bind, map_mul, ihx, ihy]) }
id ┴ └┘ └──────┘ └─────┘ └┘ ┴ ┴ └─┘ └─┘ └──────┘ └─────┘ └─┘ └─┘
src └──┘└──────┘└┘└─────┘└┘ ┴ └──┘└──────┘└┘└─────┘└┘ └┘ ┴
typ ┴ └┘ └──┘└──────┘└┘└─────┘└┘└┘┴ ┴ ┴ └─┘ └─┘ └──┘└──────┘└┘└─────┘└┘└─┘└┘└─┘┴
doc └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘ ┴
st └───────────┘└───────┘└──┘┴ └───────────┘└───────┘└───┘└───┘┴
646
647 end category
648
649 section reduce
650
651 variable [decidable_eq α]
id └──────────┘
src └──────────┘
typ └──────────┘
652
653 /-- The maximal reduction of a word. It is computable
654 iff `α` has decidable equality. -/
655 def reduce (L : list (α × bool)) : list (α × bool) :=
id └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘
src └──┘ ┴ └──┘ └──┘ ┴ └──┘
typ └──┘ ┴ ┴ └──┘ └──┘ ┴ ┴ └──┘
656 list.rec_on L [] $ λ hd1 tl1 ih,
id └─────────┘ ┴ └┘ └─┘ └─┘ └┘
src └─────────┘ └┘
typ └─────────┘ ┴ └┘ └─┘ └─┘ └┘
657 list.cases_on ih [hd1] $ λ hd2 tl2,
id └───────────┘ └┘ ┴└─┘┴ └─┘ └─┘
src └───────────┘ ┴ ┴
typ └───────────┘ └┘ ┴└─┘┴ └─┘ └─┘
658 if hd1.1 = hd2.1 ∧ hd1.2 = bnot hd2.2 then tl2
id └─┘┴ ┴ └─┘┴ ┴ └─┘┴ ┴ └──┘ └─┘┴ └─┘
src ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
typ └─┘┴ ┴ └─┘┴ ┴ └─┘┴ ┴ └──┘ └─┘┴ └─┘
659 else hd1 :: hd2 :: tl2
id └─┘ └┘ └─┘ └┘ └─┘
src └┘ └┘
typ └─┘ └┘ └─┘ └┘ └─┘
660
661 @[simp] lemma reduce.cons (x) : reduce (x :: L) =
id └────┘ ┴ └┘ ┴ ┴
src └────┘ └┘ ┴
typ └────┘ ┴ └┘ ┴ ┴
doc └──┘ └────┘
662 list.cases_on (reduce L) [x] (λ hd tl,
id └───────────┘ └────┘ ┴ ┴┴┴ └┘ └┘
src └───────────┘ └────┘ ┴ ┴
typ └───────────┘ └────┘ ┴ ┴┴┴ └┘ └┘
doc └────┘
663 if x.1 = hd.1 ∧ x.2 = bnot hd.2 then tl
id ┴┴ ┴ └┘┴ ┴ ┴┴ ┴ └──┘ └┘┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
typ ┴┴ ┴ └┘┴ ┴ ┴┴ ┴ └──┘ └┘┴ └┘
664 else x :: hd :: tl) := rfl
id ┴ └┘ └┘ └┘ └┘ └─┘
src └┘ └┘ └─┘
typ ┴ └┘ └┘ └┘ └┘ └─┘
665
666 /-- The first theorem that characterises the function
667 `reduce`: a word reduces to its maximal reduction. -/
668 theorem reduce.red : red L (reduce L) :=
id └─┘ ┴ └────┘ ┴
src └─┘ └────┘
typ └─┘ ┴ └────┘ ┴
doc └─┘ └────┘
669 begin
st └─────
670 induction L with hd1 tl1 ih,
id ┴
src └────────┘ └──────────────┘
typ └────────┘┴└──────────────┘
doc └────────┘ └──────────────┘
txt └────────┘ └──────────────┘
par └────────┘ └──────────────┘
pid ┴ ┴└─────────────┘
st ────────────────────────────┘└─
671 case list.nil
src └─────────────
typ └─────────────
doc └─────────────
txt └─────────────
par └─────────────
pid └───────┘└
st ────────────────
672 { constructor },
src ───┘└──────────┘┴
typ ───┘└──────────┘┴
doc ───┘└──────────┘┴
txt ───┘└──────────┘┴
par ───┘└──────────┘┴
pid ─┘└─────────────┘
st ──┘└───────────┘└┘└
673 case list.cons
src └──────────────
typ └──────────────
doc └──────────────
txt └──────────────
par └──────────────
pid └────────┘└
st ─────────────────
674 { dsimp,
src ───┘└───┘└─
typ ───┘└───┘└─
doc ───┘└───┘└─
txt ───┘└───┘└─
par ───┘└───┘└─
pid ─┘└────────
st ────────┘└─
675 revert ih,
src ───┘└───────┘└─
typ ───┘└───────┘└─
doc ───┘└───────┘└─
txt ───┘└───────┘└─
par ───┘└───────┘└─
pid ───────────────
st ────────────┘└─
676 generalize htl : reduce tl1 = TL,
id └────┘ └─┘
src ───┘└───────────────┘└────┘┴ ┴ ┴ └─
typ ───┘└───────────────┘└────┘┴└─┘┴ ┴ └─
doc ───┘└───────────────┘└────┘┴ ┴ ┴ └─
txt ───┘└───────────────┘ ┴ ┴ ┴ └─
par ───┘└───────────────┘ ┴ ┴ ┴ └─
pid ────────────────────┘ ┴ ┴ ┴ └─
st ───────────────────────────────────┘└─
677 intro ih,
src ───┘└──────┘└─
typ ───┘└──────┘└─
doc ───┘└──────┘└─
txt ───┘└──────┘└─
par ───┘└──────┘└─
pid ──────────────
st ───────────┘└─
678 cases TL with hd2 tl2,
id └┘
src ───┘└────┘ └───────────┘└─
typ ───┘└────┘└┘└───────────┘└─
doc ───┘└────┘ └───────────┘└─
txt ───┘└────┘ └───────────┘└─
par ───┘└────┘ └───────────┘└─
pid ─────────┘ └──────────────
st ────────────────────────┘└─
679 case list.nil
src ──────────────────
typ ──────────────────
doc ──────────────────
txt ──────────────────
par ──────────────────
pid ──────────────────
st ──────────────────
680 { exact red.cons_cons ih },
id └───────────┘ └┘
src ─────┘└────┘└───────────┘┴ ┴└──
typ ─────┘└────┘└───────────┘┴└┘┴└──
doc ─────┘└────┘ ┴ ┴└──
txt ─────┘└────┘ ┴ ┴└──
par ─────┘└────┘ ┴ ┴└──
pid ───────────┘ ┴ └───
st ────┘└──────────────────────┘┴└─
681 case list.cons
src ───────────────────
typ ───────────────────
doc ───────────────────
txt ───────────────────
par ───────────────────
pid ───────────────────
st ───────────────────
682 { dsimp,
src ─────┘└───┘└─
typ ─────┘└───┘└─
doc ─────┘└───┘└─
txt ─────┘└───┘└─
par ─────┘└───┘└─
pid ─────────────
st ──────────┘└─
683 by_cases h : hd1.fst = hd2.fst ∧ hd1.snd = bnot (hd2.snd),
id └─────┘ └─────┘ └─────┘ └──┘ └─────┘
src ─────┘└───────┘ └─┘└─────┘┴ ┴└─────┘┴ ┴└─────┘┴ ┴└──┘┴ └─────┘┴└─
typ ─────┘└───────┘ └─┘└─────┘┴ ┴└─────┘┴ ┴└─────┘┴ ┴└──┘┴ └─────┘┴└─
doc ─────┘└───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─
txt ─────┘└───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─
par ─────┘└───────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─
pid ──────────────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ──────────────────────────────────────────────────────────────┘└─
684 { rw [if_pos h],
id └────┘ ┴
src ───────┘└──┘└────┘┴ ┴└─
typ ───────┘└──┘└────┘┴┴┴└─
doc ───────┘└──┘ ┴ ┴└─
txt ───────┘└──┘ ┴ ┴└─
par ───────┘└──┘ ┴ ┴└─
pid ───────────┘ ┴ └──
st ──────┘└───────────┘└──
685 transitivity,
src ───────┘└──────────┘└─
typ ───────┘└──────────┘└─
doc ───────┘└──────────┘└─
txt ───────┘└──────────┘└─
par ───────┘└──────────┘└─
pid ──────────────────────
st ───────────────────┘└─
686 { exact red.cons_cons ih },
id └───────────┘ └┘
src ─────────┘└────┘└───────────┘┴ ┴└──
typ ─────────┘└────┘└───────────┘┴└┘┴└──
doc ─────────┘└────┘ ┴ ┴└──
txt ─────────┘└────┘ ┴ ┴└──
par ─────────┘└────┘ ┴ ┴└──
pid ───────────────┘ ┴ └───
st ────────┘└──────────────────────┘┴└─
687 { cases hd1, cases hd2, cases h,
id └─┘ └─┘ ┴
src ─────────┘└────┘ └┘└────┘ └┘└────┘ └─
typ ─────────┘└────┘└─┘└┘└────┘└─┘└┘└────┘┴└─
doc ─────────┘└────┘ └┘└────┘ └┘└────┘ └─
txt ─────────┘└────┘ └┘└────┘ └┘└────┘ └─
par ─────────┘└────┘ └┘└────┘ └┘└────┘ └─
pid ───────────────┘ └──────┘ └──────┘ └─
st ──────────────────┘└─────────┘└───────┘└─
688 dsimp at *, subst_vars,
src ─────────┘└────────┘└┘└────────┘└─
typ ─────────┘└────────┘└┘└────────┘└─
doc ─────────┘└────────┘└┘└────────┘└─
txt ─────────┘└────────┘└┘└────────┘└─
par ─────────┘└────────┘└┘└────────┘└─
pid ──────────────────────────────────
st ───────────────────┘└──────────┘└─
689 exact red.step.cons_bnot_rev.to_red } },
id └───────────────────────────┘
src ─────────┘└────┘└───────────────────────────┘┴└────
typ ─────────┘└────┘└───────────────────────────┘┴└────
doc ─────────┘└────┘ ┴└────
txt ─────────┘└────┘ ┴└────
par ─────────┘└────┘ ┴└────
pid ───────────────┘ └─────
st ─────────────────────────────────────────────┘└─┘└─
690 { rw [if_neg h],
id └────┘ ┴
src ───────┘└──┘└────┘┴ ┴└─
typ ───────┘└──┘└────┘┴┴┴└─
doc ───────┘└──┘ ┴ ┴└─
txt ───────┘└──┘ ┴ ┴└─
par ───────┘└──┘ ┴ ┴└─
pid ───────────┘ ┴ └──
st ───────────────────┘└──
691 exact red.cons_cons ih } } }
id └───────────┘ └┘
src ───────┘└────┘└───────────┘┴ ┴└────┘
typ ───────┘└────┘└───────────┘┴└┘┴└────┘
doc ───────┘└────┘ ┴ ┴└────┘
txt ───────┘└────┘ ┴ ┴└────┘
par ───────┘└────┘ ┴ ┴└────┘
pid ─────────────┘ ┴ └────┘┴
st ──────────────────────────────┘└─┘┴┴┴
692 end
st └─┘
693
694 theorem reduce.not {p : Prop} : ∀ {L₁ L₂ L₃ : list (α × bool)} {x b}, reduce L₁ = L₂ ++ (x, b) :: (x, bnot b) :: L₃ → p
id ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └────┘ └┘ ┴ └┘ └┘ ┴┴ ┴ └┘ ┴┴ └──┘ ┴ └┘ └┘ ┴
src └──┘ ┴ └──┘ └────┘ ┴ └┘ ┴ └┘ ┴ └──┘ └┘
typ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └────┘ └┘ ┴ └┘ └┘ ┴┴ ┴ └┘ ┴┴ └──┘ ┴ └┘ └┘ ┴
doc └────┘
695 | [] L2 L3 _ _ := λ h, by cases L2; injections
id └┘ ┴ └┘
src └┘ └────┘ └─────────┘
typ └┘ ┴ └────┘└┘ └─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ ┴
st └────────────────────┘
696 | ((x,b)::L1) L2 L3 x' b' := begin
id ┴ └┘
src ┴ └┘
typ ┴ └┘
st └─────
697 dsimp,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
698 cases r : reduce L1,
id └────┘ └┘
src └────┘ └─┘└────┘┴
typ └────┘ └─┘└────┘┴└┘
doc └────┘ └─┘└────┘┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ────────────────────┘└─
699 { dsimp, intro h,
src └───┘ └─────┘
typ └───┘ └─────┘
doc └───┘ └─────┘
txt └───┘ └─────┘
par └───┘ └─────┘
pid └┘
st ───┘└───┘└───────┘└─
700 have := congr_arg list.length h,
id └───────┘ └─────────┘ ┴
src └──────┘└───────┘┴└─────────┘┴
typ └──────┘└───────┘┴└─────────┘┴┴
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st ──────────────────────────────────┘└─
701 simp [-add_comm] at this,
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
txt └──────────────────────┘
par └──────────────────────┘
pid ┴└─────────┘┴└─────┘
st ───────────────────────────┘└─
702 exact absurd this dec_trivial },
id └────┘ └──┘ └─────────┘
src └────┘└────┘┴ ┴└─────────┘┴
typ └────┘└────┘┴└──┘┴└─────────┘┴
doc └────┘ ┴ ┴└─────────┘┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────┘└┘└
703 cases hd with y c,
id └┘
src └────┘ └───────┘
typ └────┘└┘└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ──────────────────┘└─
704 by_cases x = y ∧ b = bnot c; simp [h]; intro H,
id ┴ ┴ ┴ └──┘ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘┴ └────┘ ┴ └─────┘
typ └───────┘┴┴ ┴┴┴ ┴┴┴ ┴└──┘┴┴ └────┘┴┴ └─────┘
doc └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └─────┘
txt └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └─────┘
par └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └─────┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └┘
st ───────────────────────────────────────────────┘└─
705 { rw H at r,
id ┴
src └─┘ └───┘
typ └─┘┴└───┘
doc └─┘ └───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ───┘└───────┘└─
706 exact @reduce.not L1 ((y,c)::L2) L3 x' b' r },
id └────────┘ └┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴
src └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
typ └────┘ └────────┘┴└┘┴ ┴┴┴┴ └┘└┘└┘┴└┘┴└┘┴┴┴
doc └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────┘└┘└
707 rcases L2 with _|⟨a, L2⟩,
id └┘
src └─────┘ └─────────────┘
typ └─────┘└┘└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st ─────────────────────────┘└─
708 { injections, subst_vars,
src └────────┘ └────────┘
typ └────────┘ └────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
st ───┘└────────┘└──────────┘└─
709 simp at h, cc },
src └───────┘ └─┘
typ └───────┘ └─┘
doc └───────┘ └─┘
txt └───────┘ └─┘
par └───────┘ └─┘
pid ┴└──┘ ┴
st ────────────┘└───┘└┘└
710 { refine @reduce.not L1 L2 L3 x' b' _,
id └────────┘ └┘ └┘ └┘ └┘ └┘
src └─────┘ ┴ ┴ ┴ ┴ ┴ └┘
typ └─────┘ └────────┘┴└┘┴└┘┴└┘┴└┘┴└┘└┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────┘└─
711 injection H with _ H,
id ┴
src └────────┘ └───────┘
typ └────────┘┴└───────┘
doc └────────┘ └───────┘
txt └────────┘ └───────┘
par └────────┘ └───────┘
pid ┴ └───────┘
st ───────────────────────┘└─
712 rw [r, H], refl }
id ┴ ┴
src └──┘ └┘ ┴ └───┘
typ └──┘┴└┘┴┴ └───┘
doc └──┘ └┘ ┴ └───┘
txt └──┘ └┘ ┴ └───┘
par └──┘ └┘ ┴ └───┘
pid └┘ └┘ ┴ ┴
st ────────┘└─┘└──────┘└─
713 end
st ──┘
714
715 /-- The second theorem that characterises the
716 function `reduce`: the maximal reduction of a word
717 only reduces to itself. -/
718 theorem reduce.min (H : red (reduce L₁) L₂) : reduce L₁ = L₂ :=
id └─┘ └────┘ └┘ └┘ └────┘ └┘ ┴ └┘
src └─┘ └────┘ └────┘ ┴
typ └─┘ └────┘ └┘ └┘ └────┘ └┘ ┴ └┘
doc └─┘ └────┘ └────┘
719 begin
st └─────
720 induction H with L1 L' L2 H1 H2 ih,
id ┴
src └────────┘ └─────────────────────┘
typ └────────┘┴└─────────────────────┘
doc └────────┘ └─────────────────────┘
txt └────────┘ └─────────────────────┘
par └────────┘ └─────────────────────┘
pid ┴ ┴└────────────────────┘
st ───────────────────────────────────┘└─
721 { refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ───┘└───┘└┘└
722 { cases H1 with L4 L5 x b,
id └┘
src └────┘ └─────────────┘
typ └────┘└┘└─────────────┘
doc └────┘ └─────────────┘
txt └────┘ └─────────────┘
par └────┘ └─────────────┘
pid ┴ └─────────────┘
st ──────────────────────────┘└─
723 exact reduce.not H2 }
id └────────┘ └┘
src └────┘└────────┘┴ ┴
typ └────┘└────────┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────────────┘└─
724 end
st ──┘
725
726 /-- `reduce` is idempotent, i.e. the maximal reduction
727 of the maximal reduction of a word is the maximal
728 reduction of the word. -/
729 theorem reduce.idem : reduce (reduce L) = reduce L :=
id └────┘ └────┘ ┴ ┴ └────┘ ┴
src └────┘ └────┘ ┴ └────┘
typ └────┘ └────┘ ┴ ┴ └────┘ ┴
doc └────┘ └────┘ └────┘
730 eq.symm $ reduce.min reduce.red
id └─────┘ └────────┘ └────────┘
src └─────┘ └────────┘ └────────┘
typ └─────┘ └────────┘ └────────┘
doc └────────┘ └────────┘
731
732 theorem reduce.step.eq (H : red.step L₁ L₂) : reduce L₁ = reduce L₂ :=
id └──────┘ └┘ └┘ └────┘ └┘ ┴ └────┘ └┘
src └──────┘ └────┘ ┴ └────┘
typ └──────┘ └┘ └┘ └────┘ └┘ ┴ └────┘ └┘
doc └──────┘ └────┘ └────┘
733 let ⟨L₃, HR13, HR23⟩ := red.church_rosser reduce.red (reduce.red.head H) in
id └─┘ └──┘ └──┘ └───────────────┘ └────────┘ └────────┘└───┘ ┴
src └───────────────┘ └────────┘ └────────┘└───┘
typ └─┘ └──┘ └──┘ └───────────────┘ └────────┘ └────────┘└───┘ ┴
doc └───────────────┘ └────────┘ └────────┘
734 (reduce.min HR13).trans (reduce.min HR23).symm
id └────────┘ └───┘ └────────┘ └──┘
src └────────┘ └───┘ └────────┘ └──┘
typ └────────┘ └───┘ └────────┘ └──┘
doc └────────┘ └────────┘
735
736 /-- If a word reduces to another word, then they have
737 a common maximal reduction. -/
738 theorem reduce.eq_of_red (H : red L₁ L₂) : reduce L₁ = reduce L₂ :=
id └─┘ └┘ └┘ └────┘ └┘ ┴ └────┘ └┘
src └─┘ └────┘ ┴ └────┘
typ └─┘ └┘ └┘ └────┘ └┘ ┴ └────┘ └┘
doc └─┘ └────┘ └────┘
739 let ⟨L₃, HR13, HR23⟩ := red.church_rosser reduce.red (red.trans H reduce.red) in
id └─┘ └──┘ └──┘ └───────────────┘ └────────┘ └───────┘ ┴ └────────┘
src └───────────────┘ └────────┘ └───────┘ └────────┘
typ └─┘ └──┘ └──┘ └───────────────┘ └────────┘ └───────┘ ┴ └────────┘
doc └───────────────┘ └────────┘ └────────┘
740 (reduce.min HR13).trans (reduce.min HR23).symm
id └────────┘ └───┘ └────────┘ └──┘
src └────────┘ └───┘ └────────┘ └──┘
typ └────────┘ └───┘ └────────┘ └──┘
doc └────────┘ └────────┘
741
742 /-- If two words correspond to the same element in
743 the free group, then they have a common maximal
744 reduction. This is the proof that the function that
745 sends an element of the free group to its maximal
746 reduction is well-defined. -/
747 theorem reduce.sound (H : mk L₁ = mk L₂) : reduce L₁ = reduce L₂ :=
id └┘ └┘ ┴ └┘ └┘ └────┘ └┘ ┴ └────┘ └┘
src └┘ ┴ └┘ └────┘ ┴ └────┘
typ └┘ └┘ ┴ └┘ └┘ └────┘ └┘ ┴ └────┘ └┘
doc └────┘ └────┘
748 let ⟨L₃, H13, H23⟩ := red.exact.1 H in
id └─┘ └─┘ └─┘ └───────┘┴ ┴
src └───────┘┴
typ └─┘ └─┘ └─┘ └───────┘┴ ┴
749 (reduce.eq_of_red H13).trans (reduce.eq_of_red H23).symm
id └──────────────┘ └───┘ └──────────────┘ └──┘
src └──────────────┘ └───┘ └──────────────┘ └──┘
typ └──────────────┘ └───┘ └──────────────┘ └──┘
doc └──────────────┘ └──────────────┘
750
751 /-- If two words have a common maximal reduction,
752 then they correspond to the same element in the free group. -/
753 theorem reduce.exact (H : reduce L₁ = reduce L₂) : mk L₁ = mk L₂ :=
id └────┘ └┘ ┴ └────┘ └┘ └┘ └┘ ┴ └┘ └┘
src └────┘ ┴ └────┘ └┘ ┴ └┘
typ └────┘ └┘ ┴ └────┘ └┘ └┘ └┘ ┴ └┘ └┘
doc └────┘ └────┘
754 red.exact.2 ⟨reduce L₂, H ▸ reduce.red, reduce.red⟩
id └───────┘┴ └────┘ └┘ ┴ ┴ └────────┘ └────────┘
src └───────┘┴ └────┘ ┴ └────────┘ └────────┘
typ └───────┘┴ └────┘ └┘ ┴ ┴ └────────┘ └────────┘
doc └────┘ └────────┘ └────────┘
755
756 /-- A word and its maximal reduction correspond to
757 the same element of the free group. -/
758 theorem reduce.self : mk (reduce L) = mk L :=
id └┘ └────┘ ┴ ┴ └┘ ┴
src └┘ └────┘ ┴ └┘
typ └┘ └────┘ ┴ ┴ └┘ ┴
doc └────┘
759 reduce.exact reduce.idem
id └──────────┘ └─────────┘
src └──────────┘ └─────────┘
typ └──────────┘ └─────────┘
doc └──────────┘ └─────────┘
760
761 /-- If words `w₁ w₂` are such that `w₁` reduces to `w₂`,
762 then `w₂` reduces to the maximal reduction of `w₁`. -/
763 theorem reduce.rev (H : red L₁ L₂) : red L₂ (reduce L₁) :=
id └─┘ └┘ └┘ └─┘ └┘ └────┘ └┘
src └─┘ └─┘ └────┘
typ └─┘ └┘ └┘ └─┘ └┘ └────┘ └┘
doc └─┘ └─┘ └────┘
764 (reduce.eq_of_red H).symm ▸ reduce.red
id └──────────────┘ ┴ └──┘ ┴ └────────┘
src └──────────────┘ └──┘ ┴ └────────┘
typ └──────────────┘ ┴ └──┘ ┴ └────────┘
doc └──────────────┘ └────────┘
765
766 /-- The function that sends an element of the free
767 group to its maximal reduction. -/
768 def to_word : free_group α → list (α × bool) :=
id └────────┘ ┴ └──┘ ┴ ┴ └──┘
src └────────┘ └──┘ ┴ └──┘
typ └────────┘ ┴ └──┘ ┴ ┴ └──┘
doc └────────┘
769 quot.lift reduce $ λ L₁ L₂ H, reduce.step.eq H
id └───────┘ └────┘ └┘ └┘ ┴ └────────────┘ ┴
src └────┘ └────────────┘
typ └───────┘ └────┘ └┘ └┘ ┴ └────────────┘ ┴
doc └────┘
770
771 lemma to_word.mk : ∀{x : free_group α}, mk (to_word x) = x :=
id └────────┘ ┴ └┘ └─────┘ ┴ ┴ ┴
src └────────┘ └┘ └─────┘ ┴
typ └────────┘ ┴ └┘ └─────┘ ┴ ┴ ┴
doc └────────┘ └─────┘
772 by rintros ⟨L⟩; exact reduce.self
id └─────────┘
src └─────────┘ └────┘└─────────┘└
typ └─────────┘ └────┘└─────────┘└
doc └─────────┘ └────┘└─────────┘└
txt └─────────┘ └────┘ └
par └─────────┘ └────┘ └
pid └──┘ ┴ └
st └───────────────────────────────
773
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
774 lemma to_word.inj : ∀(x y : free_group α), to_word x = to_word y → x = y :=
id └────────┘ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src └────────┘ └─────┘ ┴ └─────┘ ┴
typ └────────┘ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └────────┘ └─────┘ └─────┘
775 by rintros ⟨L₁⟩ ⟨L₂⟩; exact reduce.exact
id └──────────┘
src └───────────────┘ └────┘└──────────┘└
typ └───────────────┘ └────┘└──────────┘└
doc └───────────────┘ └────┘└──────────┘└
txt └───────────────┘ └────┘ └
par └───────────────┘ └────┘ └
pid └────────┘ ┴ └
st └──────────────────────────────────────
776
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
777 /-- Constructive Church-Rosser theorem (compare `church_rosser`). -/
778 def reduce.church_rosser (H12 : red L₁ L₂) (H13 : red L₁ L₃) :
id └─┘ └┘ └┘ └─┘ └┘ └┘
src └─┘ └─┘
typ └─┘ └┘ └┘ └─┘ └┘ └┘
doc └─┘ └─┘
779 { L₄ // red L₂ L₄ ∧ red L₃ L₄ } :=
id ┴ └┘ └─┘ └┘ └┘ ┴ └─┘ └┘ └┘
src ┴ └─┘ ┴ └─┘
typ ┴ └┘ └─┘ └┘ └┘ ┴ └─┘ └┘ └┘
doc └─┘ └─┘
780 ⟨reduce L₁, reduce.rev H12, reduce.rev H13⟩
id └────┘ └┘ └────────┘ └─┘ └────────┘ └─┘
src └────┘ └────────┘ └────────┘
typ └────┘ └┘ └────────┘ └─┘ └────────┘ └─┘
doc └────┘ └────────┘ └────────┘
781
782 instance : decidable_eq (free_group α) :=
id └──────────┘ └────────┘ ┴
src └──────────┘ └────────┘
typ └──────────┘ └────────┘ ┴
doc └────────┘
783 function.injective.decidable_eq to_word.inj
id └─────────────────────────────┘ └─────────┘
src └─────────────────────────────┘ └─────────┘
typ └─────────────────────────────┘ └─────────┘
784
785 instance red.decidable_rel : decidable_rel (@red α)
id └───────────┘ └─┘ ┴
src └───────────┘ └─┘
typ └───────────┘ └─┘ ┴
doc └─┘
786 | [] [] := is_true red.refl
id └┘ └┘ └─────┘ └──────┘
src └┘ └┘ └─────┘ └──────┘
typ └┘ └┘ └─────┘ └──────┘
787 | [] (hd2::tl2) := is_false $ λ H, list.no_confusion (red.nil_iff.1 H)
id └┘ └┘ └──────┘ ┴ └───────────────┘ └─────────┘┴ ┴
src └┘ └┘ └──────┘ └───────────────┘ └─────────┘┴
typ └┘ └┘ └──────┘ ┴ └───────────────┘ └─────────┘┴ ┴
doc └─────────┘
788 | ((x,b)::tl) [] := match red.decidable_rel tl [(x, bnot b)] with
id ┴┴ ┴ └┘└┘ └┘ └───────────────┘ ┴┴ └──┘ ┴
src ┴ └┘ └┘ ┴┴ └──┘ ┴
typ ┴┴ ┴ └┘└┘ └┘ └───────────────┘ ┴┴ └──┘ ┴
789 | is_true H := is_true $ red.trans (red.cons_cons H) $
id └─────┘ ┴ └─────┘ └───────┘ └───────────┘
src └─────┘ └─────┘ └───────┘ └───────────┘
typ └─────┘ ┴ └─────┘ └───────┘ └───────────┘
790 (@red.step.bnot _ [] [] _ _).to_red
id └───────────┘ └┘ └┘ └────┘
src └───────────┘ └┘ └┘ └────┘
typ └───────────┘ └┘ └┘ └────┘
791 | is_false H := is_false $ λ H2, H $ red.cons_nil_iff_singleton.1 H2
id └──────┘ ┴ └──────┘ └┘ └────────────────────────┘┴ └┘
src └──────┘ └──────┘ └────────────────────────┘┴
typ └──────┘ ┴ └──────┘ └┘ └────────────────────────┘┴ └┘
doc └────────────────────────┘
792 end
793 | ((x1,b1)::tl1) ((x2,b2)::tl2) := if h : (x1, b1) = (x2, b2)
id ┴└┘ └┘ └┘└─┘ ┴└┘ └┘ └┘└─┘ └┘ ┴ ┴ ┴
src ┴ └┘ ┴ └┘ └┘ ┴ ┴ ┴
typ ┴└┘ └┘ └┘└─┘ ┴└┘ └┘ └┘└─┘ └┘ ┴ ┴ ┴
794 then match red.decidable_rel tl1 tl2 with
id └───────────────┘
typ └───────────────┘
795 | is_true H := is_true $ h ▸ red.cons_cons H
id └─────┘ ┴ └─────┘ ┴ ┴ └───────────┘
src └─────┘ └─────┘ ┴ └───────────┘
typ └─────┘ ┴ └─────┘ ┴ ┴ └───────────┘
796 | is_false H := is_false $ λ H2, H $ h ▸ (red.cons_cons_iff _).1 $ H2
id └──────┘ ┴ └──────┘ └┘ ┴ ┴ └───────────────┘ ┴ └┘
src └──────┘ └──────┘ ┴ └───────────────┘ ┴
typ └──────┘ ┴ └──────┘ └┘ ┴ ┴ └───────────────┘ ┴ └┘
797 end
798 else match red.decidable_rel tl1 ((x1,bnot b1)::(x2,b2)::tl2) with
id └───┘ └───────────────┘ ┴ └──┘ └┘┴ └┘
src └───┘ ┴ └──┘ └┘┴ └┘
typ └───┘ └───────────────┘ ┴ └──┘ └┘┴ └┘
799 | is_true H := is_true $ (red.cons_cons H).tail red.step.cons_bnot
id └─────┘ ┴ └─────┘ └───────────┘ └──┘ └────────────────┘
src └─────┘ └─────┘ └───────────┘ └──┘ └────────────────┘
typ └─────┘ ┴ └─────┘ └───────────┘ └──┘ └────────────────┘
800 | is_false H := is_false $ λ H2, H $ red.inv_of_red_of_ne h H2
id └──────┘ ┴ └──────┘ └┘ └──────────────────┘ ┴ └┘
src └──────┘ └──────┘ └──────────────────┘
typ └──────┘ ┴ └──────┘ └┘ └──────────────────┘ ┴ └┘
doc └──────────────────┘
801 end
802
803 /-- A list containing every word that `w₁` reduces to. -/
804 def red.enum (L₁ : list (α × bool)) : list (list (α × bool)) :=
id └──┘ ┴ ┴ └──┘ └──┘ └──┘ ┴ ┴ └──┘
src └──┘ ┴ └──┘ └──┘ └──┘ ┴ └──┘
typ └──┘ ┴ ┴ └──┘ └──┘ └──┘ ┴ ┴ └──┘
805 list.filter (λ L₂, red L₁ L₂) (list.sublists L₁)
id └─────────┘ └┘ └─┘ └┘ └┘ └───────────┘ └┘
src └─────────┘ └─┘ └───────────┘
typ └─────────┘ └┘ └─┘ └┘ └┘ └───────────┘ └┘
doc └─┘ └───────────┘
806
807 theorem red.enum.sound (H : L₂ ∈ red.enum L₁) : red L₁ L₂ :=
id └┘ ┴ └──────┘ └┘ └─┘ └┘ └┘
src ┴ └──────┘ └─┘
typ └┘ ┴ └──────┘ └┘ └─┘ └┘ └┘
doc └──────┘ └─┘
808 list.of_mem_filter H
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
809
810 theorem red.enum.complete (H : red L₁ L₂) : L₂ ∈ red.enum L₁ :=
id └─┘ └┘ └┘ └┘ ┴ └──────┘ └┘
src └─┘ ┴ └──────┘
typ └─┘ └┘ └┘ └┘ ┴ └──────┘ └┘
doc └─┘ └──────┘
811 list.mem_filter_of_mem (list.mem_sublists.2 $ red.sublist H) H
id └────────────────────┘ └───────────────┘┴ └─────────┘ ┴ ┴
src └────────────────────┘ └───────────────┘┴ └─────────┘
typ └────────────────────┘ └───────────────┘┴ └─────────┘ ┴ ┴
doc └─────────┘
812
813 instance : fintype { L₂ // red L₁ L₂ } :=
id └─────┘ ┴ └┘ └─┘ └┘ └┘
src └─────┘ ┴ └─┘
typ └─────┘ ┴ └┘ └─┘ └┘ └┘
doc └─────┘ └─┘
814 fintype.subtype (list.to_finset $ red.enum L₁) $
id └─────────────┘ └────────────┘ └──────┘ └┘
src └─────────────┘ └────────────┘ └──────┘
typ └─────────────┘ └────────────┘ └──────┘ └┘
doc └────────────┘ └──────┘
815 λ L₂, ⟨λ H, red.enum.sound $ list.mem_to_finset.1 H,
id └┘ ┴ └────────────┘ └────────────────┘┴ ┴
src └────────────┘ └────────────────┘┴
typ └┘ ┴ └────────────┘ └────────────────┘┴ ┴
816 λ H, list.mem_to_finset.2 $ red.enum.complete H⟩
id ┴ └────────────────┘┴ └───────────────┘ ┴
src └────────────────┘┴ └───────────────┘
typ ┴ └────────────────┘┴ └───────────────┘ ┴
817
818 end reduce
819
820 end free_group